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  7223  f1dom3el3dif  7224  xpord3inddlem  8104  elfiun  9343  prinfzo0  13653  fvf1tp  13748  lcmfunsnlem2lem2  16608  estrreslem2  18104  ostth  27602  noextendlt  27633  ltssolem1  27639  nodense  27656  btwncolg1  28623  hlln  28675  btwnlng1  28687  constrllcllem  33896  colineartriv1  36249  weiunso  36648  fnwe2lem3  43480  dfxlim2v  46275  gpgprismgriedgdmss  48528  gpgedgvtx0  48537  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgprismgr4cycllem3  48573  eenglngeehlnmlem2  49214