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  7243  f1dom3el3dif  7244  xpord3inddlem  8133  elfiun  9381  prinfzo0  13659  fvf1tp  13751  lcmfunsnlem2lem2  16609  estrreslem2  18099  ostth  27550  noextendlt  27581  sltsolem1  27587  nodense  27604  btwncolg1  28482  hlln  28534  btwnlng1  28546  constrllcllem  33742  colineartriv1  36055  weiunso  36454  fnwe2lem3  43041  dfxlim2v  45845  gpgprismgriedgdmss  48043  gpgedgvtx0  48052  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgprismgr4cycllem3  48087  eenglngeehlnmlem2  48727