Theorem 3mix3d 1339

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix3d	⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Proof of Theorem 3mix3d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix3 1333	. 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:  xpord3inddlem  8133  elfiun  9381  nnnegz  12532  fvf1tp  13751  hashv01gt1  14310  lcmfunsnlem2lem2  16609  cshwshashlem1  17066  dyaddisjlem  25496  zabsle1  27207  noextendgt  27582  sltsolem1  27587  nodense  27604  btwncolg3  28484  btwnlng3  28548  frgr3vlem2  30203  3vfriswmgr  30207  frgrregorufr0  30253  constrcccllem  33744  weiunso  36454  fnwe2lem3  43041  omcl2  43322  gpgprismgriedgdmss  48043  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg3kgrtriexlem6  48079  gpgprismgr4cycllem3  48087  eenglngeehlnmlem2  48727