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  7270  f1dom3el3dif  7271  xpord3inddlem  8145  elfiun  9431  prinfzo0  13678  lcmfunsnlem2lem2  16583  estrreslem2  18100  ostth  27485  noextendlt  27515  sltsolem1  27521  nodense  27538  btwncolg1  28239  hlln  28291  btwnlng1  28303  colineartriv1  35509  fnwe2lem3  42257  dfxlim2v  45022  eenglngeehlnmlem2  47586