MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3mix2 Structured version   Visualization version   GIF version

Theorem 3mix2 1368
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3mix2 (𝜑 → (𝜓𝜑𝜒))

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1367 . 2 (𝜑 → (𝜑𝜒𝜓))
2 3orrot 1077 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜒𝜓))
31, 2sylibr 224 1 (𝜑 → (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-or 384  df-3or 1073
This theorem is referenced by:  3mix2i  1371  3mix2d  1374  3jaob  1503  tppreqb  4444  tpres  6582  onzsl  7163  sornom  9212  nn0le2is012  11554  hash1to3  13386  cshwshashlem1  15925  zabsle1  25141  ostth  25448  nolesgn2o  32051  sltsolem1  32053  nosep1o  32059  nodenselem8  32068  fnwe2lem3  38041  dfxlim2v  40493
  Copyright terms: Public domain W3C validator