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

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

Proof of Theorem 3mix1d
StepHypRef Expression
1 3mixd.1 . 2 (𝜑𝜓)
2 3mix1 1327 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 17 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1083
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 845  df-3or 1085
This theorem is referenced by:  f1dom3fv3dif  7018  f1dom3el3dif  7019  elfiun  8891  prinfzo0  13080  lcmfunsnlem2lem2  15981  estrreslem2  17388  ostth  26229  btwncolg1  26355  hlln  26407  btwnlng1  26419  noextendlt  33236  sltsolem1  33240  nodense  33256  colineartriv1  33588  fnwe2lem3  39916  dfxlim2v  42419  eenglngeehlnmlem2  45082
  Copyright terms: Public domain W3C validator