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

Theorem 3mix1d 1420
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 1414 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 17 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1070
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 837  df-3or 1072
This theorem is referenced by:  f1dom3fv3dif  6671  f1dom3el3dif  6672  elfiun  8496  prinfzo0  12715  lcmfunsnlem2lem2  15560  estrreslem2  16985  ostth  25549  btwncolg1  25671  hlln  25723  btwnlng1  25735  noextendlt  32159  sltsolem1  32163  nodense  32179  colineartriv1  32511  fnwe2lem3  38148  dfxlim2v  40588
  Copyright terms: Public domain W3C validator