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

Theorem 3mix3d 1340
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 1334 . 2 (𝜓 → (𝜒𝜃𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1088
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 210  df-or 848  df-3or 1090
This theorem is referenced by:  elfiun  9071  nnnegz  12204  hashv01gt1  13936  lcmfunsnlem2lem2  16221  cshwshashlem1  16674  dyaddisjlem  24516  zabsle1  26201  btwncolg3  26672  btwnlng3  26736  frgr3vlem2  28381  3vfriswmgr  28385  frgrregorufr0  28431  xpord3ind  33563  noextendgt  33636  sltsolem1  33641  nodense  33658  fnwe2lem3  40609  eenglngeehlnmlem2  45786
  Copyright terms: Public domain W3C validator