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

Theorem 3mix2d 1229
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 1223 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 1 (𝜑 → (𝜒𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1029
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 195  df-or 383  df-3or 1031
This theorem is referenced by:  sosn  5100  funtpgOLD  5842  f1dom3fv3dif  6402  f1dom3el3dif  6403  elfiun  8196  fpwwe2lem13  9320  lcmfunsnlem2lem2  15138  dyaddisjlem  23113  tgcolg  25194  btwncolg2  25196  hlln  25247  btwnlng2  25260  frgraregorufr0  26372  sltsolem1  30860  colineartriv2  31138  frgrregorufr0  41470
  Copyright terms: Public domain W3C validator