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 206  df-or 845  df-3or 1087

This theorem is referenced by:  f1dom3fv3dif  7138  f1dom3el3dif  7139  elfiun  9167  prinfzo0  13424  lcmfunsnlem2lem2  16342  estrreslem2  17853  ostth  26785  btwncolg1  26914  hlln  26966  btwnlng1  26978  xpord3ind  33796  noextendlt  33868  sltsolem1  33874  nodense  33891  colineartriv1  34365  fnwe2lem3  40874  dfxlim2v  43359  eenglngeehlnmlem2  46053