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 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 207  df-or 848  df-3or 1087

This theorem is referenced by:  f1dom3fv3dif  7289  f1dom3el3dif  7290  xpord3inddlem  8180  elfiun  9471  prinfzo0  13739  fvf1tp  13830  lcmfunsnlem2lem2  16677  estrreslem2  18184  ostth  27684  noextendlt  27715  sltsolem1  27721  nodense  27738  btwncolg1  28564  hlln  28616  btwnlng1  28628  colineartriv1  36069  weiunso  36468  fnwe2lem3  43069  dfxlim2v  45867  gpgedgvtx0  48024  gpgvtxedg0  48026  gpgvtxedg1  48027  eenglngeehlnmlem2  48664