MPE Home 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 206  df-or 846  df-3or 1085
This theorem is referenced by:  sosn  5766  f1dom3fv3dif  7282  f1dom3el3dif  7283  xpord3inddlem  8163  elfiun  9459  fpwwe2lem12  10671  swrdnd0  14645  lcmfunsnlem2lem2  16615  dyaddisjlem  25542  sltsolem1  27626  tgcolg  28376  btwncolg2  28378  hlln  28429  btwnlng2  28442  frgrregorufr0  30152  colineartriv2  35669  eenglngeehlnmlem2  47862
  Copyright terms: Public domain W3C validator