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

Theorem 3mix3d 1231
 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 1225 . 2 (𝜓 → (𝜒𝜃𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1030 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 196  df-or 384  df-3or 1032 This theorem is referenced by:  funtpgOLD  5857  elfiun  8219  nnnegz  11257  hashv01gt1  12995  lcmfunsnlem2lem2  15190  cshwshashlem1  15640  dyaddisjlem  23169  zabsle1  24821  btwncolg3  25252  btwnlng3  25316  frgra3vlem2  26528  3vfriswmgra  26532  frgraregorufr0  26579  2spotdisj  26588  sltsolem1  31067  nodense  31088  fnwe2lem3  36640  frgr3vlem2  41444  3vfriswmgr  41448  frgrregorufr0  41489
 Copyright terms: Public domain W3C validator