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

Theorem 3mix1d 1256
 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 1250 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 17 1 (𝜑 → (𝜓𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1053 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 384  df-3or 1055 This theorem is referenced by:  f1dom3fv3dif  6565  f1dom3el3dif  6566  elfiun  8377  prinfzo0  12546  lcmfunsnlem2lem2  15399  estrreslem2  16825  ostth  25373  btwncolg1  25495  hlln  25547  btwnlng1  25559  noextendlt  31947  sltsolem1  31951  nodense  31967  colineartriv1  32299  fnwe2lem3  37939  dfxlim2v  40391
 Copyright terms: Public domain W3C validator