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  7224  f1dom3el3dif  7225  xpord3inddlem  8106  elfiun  9345  prinfzo0  13626  fvf1tp  13721  lcmfunsnlem2lem2  16578  estrreslem2  18073  ostth  27618  noextendlt  27649  ltssolem1  27655  nodense  27672  btwncolg1  28639  hlln  28691  btwnlng1  28703  constrllcllem  33930  colineartriv1  36283  weiunso  36682  fnwe2lem3  43409  dfxlim2v  46205  gpgprismgriedgdmss  48412  gpgedgvtx0  48421  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgprismgr4cycllem3  48457  eenglngeehlnmlem2  49098