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  7214  f1dom3el3dif  7215  xpord3inddlem  8096  elfiun  9333  prinfzo0  13614  fvf1tp  13709  lcmfunsnlem2lem2  16566  estrreslem2  18061  ostth  27606  noextendlt  27637  ltssolem1  27643  nodense  27660  btwncolg1  28627  hlln  28679  btwnlng1  28691  constrllcllem  33909  colineartriv1  36261  weiunso  36660  fnwe2lem3  43294  dfxlim2v  46091  gpgprismgriedgdmss  48298  gpgedgvtx0  48307  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgprismgr4cycllem3  48343  eenglngeehlnmlem2  48984