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  7141  f1dom3el3dif  7142  elfiun  9189  prinfzo0  13426  lcmfunsnlem2lem2  16344  estrreslem2  17855  ostth  26787  btwncolg1  26916  hlln  26968  btwnlng1  26980  xpord3ind  33800  noextendlt  33872  sltsolem1  33878  nodense  33895  colineartriv1  34369  fnwe2lem3  40877  dfxlim2v  43388  eenglngeehlnmlem2  46084