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

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

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1222 . 2 (𝜑 → (𝜑𝜒𝜓))
2 3orrot 1036 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜒𝜓))
31, 2sylibr 222 1 (𝜑 → (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1029
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 195  df-or 383  df-3or 1031
This theorem is referenced by:  3mix2i  1226  3mix2d  1229  3jaob  1381  tppreqb  4276  tpres  6348  onzsl  6915  sornom  8959  hash1to3  13080  cshwshashlem1  15588  zabsle1  24765  ostth  25072  sltsolem1  30860  nodenselem8  30880  fnwe2lem3  36423  nn0le2is012  41919
  Copyright terms: Public domain W3C validator