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

Theorem 3mix1d 1355
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 1349 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 18 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  w3o 1102
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104
This theorem is used by:  f1dom3fv3dif  7271  f1dom3el3dif  7272  xpord3inddlem  8156  elfiun  9397  prinfzo0  13744  fvf1tp  13840  lcmfunsnlem2lem2  16719  estrreslem2  18216  ostth  27854  noextendlt  27884  ltssolem1  27890  nodense  27907  btwncolg1  28875  hlln  28930  btwnlng1  28943  elplnglnid  29116  constrllcllem  34206  colineartriv1  36596  weiunso  37034  fnwe2lem3  43837  dfxlim2v  46619  gpgprismgriedgdmss  48875  gpgedgvtx0  48884  gpgvtxedg0  48886  gpgvtxedg1  48887  gpgprismgr4cycllem3  48920  eenglngeehlnmlem2  49575
  Copyright terms: Public domain W3C validator