Theorem 3mix1d 1334

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

Syntax hints:   → wi 4   ∨ w3o 1084

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 844  df-3or 1086

This theorem is referenced by:  f1dom3fv3dif  7122  f1dom3el3dif  7123  elfiun  9119  prinfzo0  13354  lcmfunsnlem2lem2  16272  estrreslem2  17771  ostth  26692  btwncolg1  26820  hlln  26872  btwnlng1  26884  xpord3ind  33727  noextendlt  33799  sltsolem1  33805  nodense  33822  colineartriv1  34296  fnwe2lem3  40793  dfxlim2v  43278  eenglngeehlnmlem2  45972