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  8136  elfiun  9388  nnnegz  12539  fvf1tp  13758  hashv01gt1  14317  lcmfunsnlem2lem2  16616  cshwshashlem1  17073  dyaddisjlem  25503  zabsle1  27214  noextendgt  27589  sltsolem1  27594  nodense  27611  btwncolg3  28491  btwnlng3  28555  frgr3vlem2  30210  3vfriswmgr  30214  frgrregorufr0  30260  constrcccllem  33751  weiunso  36461  fnwe2lem3  43048  omcl2  43329  gpgprismgriedgdmss  48047  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  gpg3kgrtriexlem6  48083  gpgprismgr4cycllem3  48091  eenglngeehlnmlem2  48731