Theorem 3mix1d 1333

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

Syntax hints:   → wi 4   ∨ w3o 1083

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 210  df-or 845  df-3or 1085

This theorem is referenced by:  f1dom3fv3dif  7004  f1dom3el3dif  7005  elfiun  8878  prinfzo0  13071  lcmfunsnlem2lem2  15973  estrreslem2  17380  ostth  26223  btwncolg1  26349  hlln  26401  btwnlng1  26413  noextendlt  33289  sltsolem1  33293  nodense  33309  colineartriv1  33641  fnwe2lem3  39996  dfxlim2v  42489  eenglngeehlnmlem2  45152