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

Theorem 3mix3d 1230
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypothesis
Ref Expression
3mixd.1 (𝜑𝜓)
Assertion
Ref Expression
3mix3d (𝜑 → (𝜒𝜃𝜓))

Proof of Theorem 3mix3d
StepHypRef Expression
1 3mixd.1 . 2 (𝜑𝜓)
2 3mix3 1224 . 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:  funtpgOLD  5839  elfiun  8192  nnnegz  11209  hashv01gt1  12943  lcmfunsnlem2lem2  15132  cshwshashlem1  15582  dyaddisjlem  23082  zabsle1  24734  btwncolg3  25166  btwnlng3  25230  frgra3vlem2  26290  3vfriswmgra  26294  frgraregorufr0  26341  2spotdisj  26350  sltsolem1  30869  nodense  30890  fnwe2lem3  36439  frgr3vlem2  41442  3vfriswmgr  41446  frgrregorufr0  41487
  Copyright terms: Public domain W3C validator