Theorem 3mix1d 1337

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 1331	. 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  7202  f1dom3el3dif  7203  xpord3inddlem  8084  elfiun  9314  prinfzo0  13598  fvf1tp  13693  lcmfunsnlem2lem2  16550  estrreslem2  18044  ostth  27577  noextendlt  27608  sltsolem1  27614  nodense  27631  btwncolg1  28533  hlln  28585  btwnlng1  28597  constrllcllem  33765  colineartriv1  36109  weiunso  36508  fnwe2lem3  43093  dfxlim2v  45893  gpgprismgriedgdmss  48091  gpgedgvtx0  48100  gpgvtxedg0  48102  gpgvtxedg1  48103  gpgprismgr4cycllem3  48136  eenglngeehlnmlem2  48778