Theorem 3mix1d 1338

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 1332	. 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 849  df-3or 1088

This theorem is referenced by:  f1dom3fv3dif  7217  f1dom3el3dif  7218  xpord3inddlem  8098  elfiun  9337  prinfzo0  13647  fvf1tp  13742  lcmfunsnlem2lem2  16602  estrreslem2  18098  ostth  27619  noextendlt  27650  ltssolem1  27656  nodense  27673  btwncolg1  28640  hlln  28692  btwnlng1  28704  constrllcllem  33915  colineartriv1  36268  weiunso  36667  fnwe2lem3  43501  dfxlim2v  46296  gpgprismgriedgdmss  48543  gpgedgvtx0  48552  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgprismgr4cycllem3  48588  eenglngeehlnmlem2  49229