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  7196  f1dom3el3dif  7197  xpord3inddlem  8078  elfiun  9308  prinfzo0  13589  fvf1tp  13681  lcmfunsnlem2lem2  16537  estrreslem2  18031  ostth  27531  noextendlt  27562  sltsolem1  27568  nodense  27585  btwncolg1  28487  hlln  28539  btwnlng1  28551  constrllcllem  33733  colineartriv1  36058  weiunso  36457  fnwe2lem3  43042  dfxlim2v  45842  gpgprismgriedgdmss  48050  gpgedgvtx0  48059  gpgvtxedg0  48061  gpgvtxedg1  48062  gpgprismgr4cycllem3  48095  eenglngeehlnmlem2  48737