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

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

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1415 . 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  1419  3mix2d  1422  3jaob  1537  tppreqb  4479  tpres  6628  onzsl  7209  sornom  9289  nn0le2is012  11631  hash1to3  13463  cshwshashlem1  16002  zabsle1  25218  ostth  25525  nolesgn2o  32128  sltsolem1  32130  nosep1o  32136  nodenselem8  32145  fnwe2lem3  38122  dfxlim2v  40574
  Copyright terms: Public domain W3C validator