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  7276  f1dom3el3dif  7277  fnwe2lem4  8155  xpord3inddlem  8178  elfiun  9429  prinfzo0  13840  fvf1tp  13936  lcmfunsnlem2lem2  16823  estrreslem2  18321  ostth  27975  noextendlt  28035  ltssolem1  28041  nodense  28058  btwncolg1  29027  hlln  29082  btwnlng1  29096  elplnglnid  29270  cgrgptxfr  33062  constrllcllem  34434  colineartriv1  36956  weiunso  37378  dfxlim2v  46993  gpgprismgriedgdmss  49286  gpgedgvtx0  49295  gpgvtxedg0  49297  gpgvtxedg1  49298  gpgprismgr4cycllem3  49331  eenglngeehlnmlem2  49987