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

Theorem 3mix2d 1334
 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 1328 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 1 (𝜑 → (𝜒𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1083 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 210  df-or 845  df-3or 1085 This theorem is referenced by:  sosn  5606  f1dom3fv3dif  7008  f1dom3el3dif  7009  elfiun  8882  fpwwe2lem13  10057  swrdnd0  14014  lcmfunsnlem2lem2  15977  dyaddisjlem  24203  tgcolg  26352  btwncolg2  26354  hlln  26405  btwnlng2  26418  frgrregorufr0  28113  sltsolem1  33294  colineartriv2  33643  eenglngeehlnmlem2  45145
 Copyright terms: Public domain W3C validator