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

Theorem 3mix3d 1423
 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 1417 . 2 (𝜓 → (𝜒𝜃𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1071 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 197  df-or 384  df-3or 1073 This theorem is referenced by:  funtpgOLD  6104  elfiun  8503  nnnegz  11592  hashv01gt1  13347  lcmfunsnlem2lem2  15574  cshwshashlem1  16024  dyaddisjlem  23583  zabsle1  25241  btwncolg3  25672  btwnlng3  25736  frgr3vlem2  27449  3vfriswmgr  27453  frgrregorufr0  27499  noextendgt  32150  sltsolem1  32153  nodense  32169  fnwe2lem3  38142
 Copyright terms: Public domain W3C validator