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 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  f1dom3fv3dif  7272  f1dom3el3dif  7273  fnwe2lem4  8148  xpord3inddlem  8171  elfiun  9422  prinfzo0  13833  fvf1tp  13929  lcmfunsnlem2lem2  16814  estrreslem2  18312  ostth  27966  noextendlt  28026  ltssolem1  28032  nodense  28049  btwncolg1  29018  hlln  29073  btwnlng1  29087  elplnglnid  29261  constrllcllem  34384  colineartriv1  36832  weiunso  37254  dfxlim2v  46856  gpgprismgriedgdmss  49149  gpgedgvtx0  49158  gpgvtxedg0  49160  gpgvtxedg1  49161  gpgprismgr4cycllem3  49194  eenglngeehlnmlem2  49849