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 206  df-or 846  df-3or 1085
This theorem is referenced by:  f1dom3fv3dif  7273  f1dom3el3dif  7274  xpord3inddlem  8158  elfiun  9464  prinfzo0  13717  lcmfunsnlem2lem2  16633  estrreslem2  18155  ostth  27663  noextendlt  27694  sltsolem1  27700  nodense  27717  btwncolg1  28477  hlln  28529  btwnlng1  28541  colineartriv1  35902  fnwe2lem3  42748  dfxlim2v  45502  eenglngeehlnmlem2  48160
  Copyright terms: Public domain W3C validator