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

Theorem 3mix2d 1422
 Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypothesis
Ref Expression
3mixd.1 (𝜑𝜓)
Assertion
Ref Expression
3mix2d (𝜑 → (𝜒𝜓𝜃))

Proof of Theorem 3mix2d
StepHypRef Expression
1 3mixd.1 . 2 (𝜑𝜓)
2 3mix2 1416 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 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:  sosn  5345  funtpgOLD  6104  f1dom3fv3dif  6688  f1dom3el3dif  6689  elfiun  8501  fpwwe2lem13  9656  lcmfunsnlem2lem2  15554  dyaddisjlem  23563  tgcolg  25648  btwncolg2  25650  hlln  25701  btwnlng2  25714  frgrregorufr0  27478  sltsolem1  32132  colineartriv2  32481
 Copyright terms: Public domain W3C validator