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

Theorem 3mix2d 1338
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 1332 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 1 (𝜑 → (𝜒𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1086
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 207  df-or 849  df-3or 1088
This theorem is referenced by:  sosn  5772  f1dom3fv3dif  7288  f1dom3el3dif  7289  xpord3inddlem  8179  elfiun  9470  fpwwe2lem12  10682  fvf1tp  13829  swrdnd0  14695  lcmfunsnlem2lem2  16676  dyaddisjlem  25630  sltsolem1  27720  tgcolg  28562  btwncolg2  28564  hlln  28615  btwnlng2  28628  frgrregorufr0  30343  constrsslem  33782  colineartriv2  36069  gpgvtxedg0  48021  gpgvtxedg1  48022  eenglngeehlnmlem2  48659
  Copyright terms: Public domain W3C validator