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

Theorem 3mix1d 1436
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 1430 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 17 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1107
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 199  df-or 875  df-3or 1109
This theorem is referenced by:  f1dom3fv3dif  6753  f1dom3el3dif  6754  elfiun  8578  prinfzo0  12762  lcmfunsnlem2lem2  15687  estrreslem2  17092  ostth  25680  btwncolg1  25806  hlln  25858  btwnlng1  25870  noextendlt  32335  sltsolem1  32339  nodense  32355  colineartriv1  32687  fnwe2lem3  38407  dfxlim2v  40817
  Copyright terms: Public domain W3C validator