Theorem 3mix3d 1345

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 1339	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  xpord3inddlem  8094  elfiun  9333  nnnegz  12518  fvf1tp  13739  hashv01gt1  14298  lcmfunsnlem2lem2  16599  cshwshashlem1  17057  dyaddisjlem  25580  zabsle1  27277  noextendgt  27652  ltssolem1  27657  nodense  27674  btwncolg3  28643  btwnlng3  28707  frgr3vlem2  30362  3vfriswmgr  30366  frgrregorufr0  30412  constrcccllem  33938  weiunso  36694  fnwe2lem3  43497  omcl2  43778  gpgprismgriedgdmss  48543  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpg3kgrtriexlem6  48579  gpgprismgr4cycllem3  48588  eenglngeehlnmlem2  49229