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  7303  f1dom3el3dif  7304  fnwe2lem4  8185  xpord3inddlem  8208  elfiun  9459  prinfzo0  13873  fvf1tp  13969  lcmfunsnlem2lem2  16858  estrreslem2  18362  ostth  28023  noextendlt  28083  ltssolem1  28089  nodense  28106  btwncolg1  29075  hlln  29130  btwnlng1  29144  elplnglnid  29318  cgrgptxfr  33110  constrllcllem  34495  colineartriv1  37047  weiunso  37469  dfxlim2v  47130  gpgprismgriedgdmss  49423  gpgedgvtx0  49432  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgprismgr4cycllem3  49468  eenglngeehlnmlem2  50182