Theorem 3mix1d 1335

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 1329	. 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  7288  f1dom3el3dif  7289  xpord3inddlem  8178  elfiun  9468  prinfzo0  13735  fvf1tp  13826  lcmfunsnlem2lem2  16673  estrreslem2  18194  ostth  27698  noextendlt  27729  sltsolem1  27735  nodense  27752  btwncolg1  28578  hlln  28630  btwnlng1  28642  colineartriv1  36049  weiunso  36449  fnwe2lem3  43041  dfxlim2v  45803  gpgedgvtx0  47954  gpgvtxedg0  47956  gpgvtxedg1  47957  eenglngeehlnmlem2  48588