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 206  df-or 846  df-3or 1085

This theorem is referenced by:  f1dom3fv3dif  7273  f1dom3el3dif  7274  xpord3inddlem  8158  elfiun  9464  prinfzo0  13717  lcmfunsnlem2lem2  16633  estrreslem2  18155  ostth  27663  noextendlt  27694  sltsolem1  27700  nodense  27717  btwncolg1  28477  hlln  28529  btwnlng1  28541  colineartriv1  35902  fnwe2lem3  42748  dfxlim2v  45502  eenglngeehlnmlem2  48160