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

Theorem 3mix3d 1339
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 1333 . 2 (𝜓 → (𝜒𝜃𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1087
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 847  df-3or 1089
This theorem is referenced by:  xpord3inddlem  8140  elfiun  9425  nnnegz  12561  hashv01gt1  14305  lcmfunsnlem2lem2  16576  cshwshashlem1  17029  dyaddisjlem  25112  zabsle1  26799  noextendgt  27173  sltsolem1  27178  nodense  27195  btwncolg3  27839  btwnlng3  27903  frgr3vlem2  29558  3vfriswmgr  29562  frgrregorufr0  29608  fnwe2lem3  41842  omcl2  42131  eenglngeehlnmlem2  47472
  Copyright terms: Public domain W3C validator