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

Theorem 3mix3d 1236
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 1230 . 2 (𝜓 → (𝜒𝜃𝜓))
31, 2syl 17 1 (𝜑 → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1035
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 385  df-3or 1037
This theorem is referenced by:  funtpgOLD  5931  elfiun  8321  nnnegz  11365  hashv01gt1  13116  lcmfunsnlem2lem2  15333  cshwshashlem1  15783  dyaddisjlem  23344  zabsle1  25002  btwncolg3  25433  btwnlng3  25497  frgr3vlem2  27118  3vfriswmgr  27122  frgrregorufr0  27162  noextendgt  31797  sltsolem1  31800  nodense  31816  fnwe2lem3  37441
  Copyright terms: Public domain W3C validator