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

Theorem 3mix2d 1230
 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 1224 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 1 (𝜑 → (𝜒𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1030 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 196  df-or 384  df-3or 1032 This theorem is referenced by:  sosn  5111  funtpgOLD  5857  f1dom3fv3dif  6425  f1dom3el3dif  6426  elfiun  8219  fpwwe2lem13  9343  lcmfunsnlem2lem2  15190  dyaddisjlem  23169  tgcolg  25249  btwncolg2  25251  hlln  25302  btwnlng2  25315  frgraregorufr0  26579  sltsolem1  31067  colineartriv2  31345  frgrregorufr0  41489
 Copyright terms: Public domain W3C validator