Theorem 3mix1d 1337

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 1331	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1085

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 207  df-or 848  df-3or 1087

This theorem is referenced by:  f1dom3fv3dif  7246  f1dom3el3dif  7247  xpord3inddlem  8136  elfiun  9388  prinfzo0  13666  fvf1tp  13758  lcmfunsnlem2lem2  16616  estrreslem2  18106  ostth  27557  noextendlt  27588  sltsolem1  27594  nodense  27611  btwncolg1  28489  hlln  28541  btwnlng1  28553  constrllcllem  33749  colineartriv1  36062  weiunso  36461  fnwe2lem3  43048  dfxlim2v  45852  gpgprismgriedgdmss  48047  gpgedgvtx0  48056  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgprismgr4cycllem3  48091  eenglngeehlnmlem2  48731