Theorem 3mix1d 1436

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

Syntax hints:   → wi 4   ∨ w3o 1107

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 199  df-or 875  df-3or 1109

This theorem is referenced by:  f1dom3fv3dif  6753  f1dom3el3dif  6754  elfiun  8578  prinfzo0  12762  lcmfunsnlem2lem2  15687  estrreslem2  17092  ostth  25680  btwncolg1  25806  hlln  25858  btwnlng1  25870  noextendlt  32335  sltsolem1  32339  nodense  32355  colineartriv1  32687  fnwe2lem3  38407  dfxlim2v  40817