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

Theorem 3mix1d 1354
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 1348 . 2 (𝜓 → (𝜓𝜒𝜃))
31, 2syl 18 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  w3o 1101
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 861  df-3or 1103
This theorem is used by:  f1dom3fv3dif  7266  f1dom3el3dif  7267  xpord3inddlem  8148  elfiun  9388  prinfzo0  13734  fvf1tp  13829  lcmfunsnlem2lem2  16703  estrreslem2  18200  ostth  27814  noextendlt  27844  ltssolem1  27850  nodense  27867  btwncolg1  28835  hlln  28890  btwnlng1  28903  elplnglnid  29076  constrllcllem  34151  colineartriv1  36567  weiunso  37005  fnwe2lem3  43807  dfxlim2v  46589  gpgprismgriedgdmss  48845  gpgedgvtx0  48854  gpgvtxedg0  48856  gpgvtxedg1  48857  gpgprismgr4cycllem3  48890  eenglngeehlnmlem2  49546
  Copyright terms: Public domain W3C validator