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

Theorem 3mix2d 1329
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypothesis
Ref Expression
3mixd.1 (𝜑𝜓)
Assertion
Ref Expression
3mix2d (𝜑 → (𝜒𝜓𝜃))

Proof of Theorem 3mix2d
StepHypRef Expression
1 3mixd.1 . 2 (𝜑𝜓)
2 3mix2 1323 . 2 (𝜓 → (𝜒𝜓𝜃))
31, 2syl 17 1 (𝜑 → (𝜒𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1078
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 208  df-or 842  df-3or 1080
This theorem is referenced by:  sosn  5631  f1dom3fv3dif  7017  f1dom3el3dif  7018  elfiun  8882  fpwwe2lem13  10052  swrdnd0  14007  lcmfunsnlem2lem2  15971  dyaddisjlem  24123  tgcolg  26267  btwncolg2  26269  hlln  26320  btwnlng2  26333  frgrregorufr0  28030  sltsolem1  33077  colineartriv2  33426  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator