Theorem 3mix1d 1336

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 207  df-or 847  df-3or 1088

This theorem is referenced by:  f1dom3fv3dif  7305  f1dom3el3dif  7306  xpord3inddlem  8195  elfiun  9499  prinfzo0  13755  fvf1tp  13840  lcmfunsnlem2lem2  16686  estrreslem2  18207  ostth  27701  noextendlt  27732  sltsolem1  27738  nodense  27755  btwncolg1  28581  hlln  28633  btwnlng1  28645  colineartriv1  36031  weiunso  36432  fnwe2lem3  43009  dfxlim2v  45768  eenglngeehlnmlem2  48472