Theorem 3mix1d 1355

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 1349	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒 ∨ 𝜃))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1102

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 210  df-or 861  df-3or 1104

This theorem is referenced by:  f1dom3fv3dif  7266  f1dom3el3dif  7267  xpord3inddlem  8146  elfiun  9386  prinfzo0  13723  fvf1tp  13818  lcmfunsnlem2lem2  16692  estrreslem2  18189  ostth  27803  noextendlt  27833  ltssolem1  27839  nodense  27856  btwncolg1  28824  hlln  28879  btwnlng1  28892  elplnglnid  29065  constrllcllem  34142  colineartriv1  36559  weiunso  36977  fnwe2lem3  43779  dfxlim2v  46561  gpgprismgriedgdmss  48817  gpgedgvtx0  48826  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgprismgr4cycllem3  48862  eenglngeehlnmlem2  49518