Theorem 3mix1d 1350

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

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix1 1344	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1097

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 209  df-or 859  df-3or 1099

This theorem is referenced by:  f1dom3fv3dif  7252  f1dom3el3dif  7253  xpord3inddlem  8134  elfiun  9376  prinfzo0  13704  fvf1tp  13799  lcmfunsnlem2lem2  16673  estrreslem2  18170  ostth  27700  noextendlt  27730  ltssolem1  27736  nodense  27753  btwncolg1  28721  hlln  28773  btwnlng1  28785  elplnglnid  28987  constrllcllem  34046  colineartriv1  36414  weiunso  36823  fnwe2lem3  43626  dfxlim2v  46418  gpgprismgriedgdmss  48671  gpgedgvtx0  48680  gpgvtxedg0  48682  gpgvtxedg1  48683  gpgprismgr4cycllem3  48716  eenglngeehlnmlem2  49357