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  7212  f1dom3el3dif  7213  xpord3inddlem  8094  elfiun  9331  prinfzo0  13612  fvf1tp  13707  lcmfunsnlem2lem2  16564  estrreslem2  18059  ostth  27604  noextendlt  27635  sltsolem1  27641  nodense  27658  btwncolg1  28576  hlln  28628  btwnlng1  28640  constrllcllem  33858  colineartriv1  36210  weiunso  36609  fnwe2lem3  43236  dfxlim2v  46033  gpgprismgriedgdmss  48240  gpgedgvtx0  48249  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgprismgr4cycllem3  48285  eenglngeehlnmlem2  48926