Theorem 3mix1d 1332

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 844  df-3or 1084

This theorem is referenced by:  f1dom3fv3dif  7028  f1dom3el3dif  7029  elfiun  8896  prinfzo0  13079  lcmfunsnlem2lem2  15985  estrreslem2  17390  ostth  26217  btwncolg1  26343  hlln  26395  btwnlng1  26407  noextendlt  33178  sltsolem1  33182  nodense  33198  colineartriv1  33530  fnwe2lem3  39659  dfxlim2v  42135  eenglngeehlnmlem2  44732