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

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

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1330 . 2 (𝜑 → (𝜑𝜒𝜓))
2 3orrot 1091 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜒𝜓))
31, 2sylibr 234 1 (𝜑 → (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1085
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 207  df-or 848  df-3or 1087
This theorem is referenced by:  3mix2i  1334  3mix2d  1337  3jaobOLD  1427  tppreqb  4811  tpres  7225  onzsl  7871  sornom  10321  nnz  12638  nn0le2is012  12686  hash1to3  14534  cshwshashlem1  17136  zabsle1  27363  ostth  27706  nolesgn2o  27739  nogesgn1o  27741  sltsolem1  27743  nosep1o  27749  nosep2o  27750  nodenselem8  27759  fnwe2lem3  43055  dfxlim2v  45814
  Copyright terms: Public domain W3C validator