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  8094  elfiun  9339  nnnegz  12493  fvf1tp  13712  hashv01gt1  14271  lcmfunsnlem2lem2  16569  cshwshashlem1  17026  dyaddisjlem  25513  zabsle1  27224  noextendgt  27599  sltsolem1  27604  nodense  27621  btwncolg3  28521  btwnlng3  28585  frgr3vlem2  30237  3vfriswmgr  30241  frgrregorufr0  30287  constrcccllem  33740  weiunso  36459  fnwe2lem3  43045  omcl2  43326  gpgprismgriedgdmss  48056  gpgedgvtx1  48066  gpgvtxedg0  48067  gpgvtxedg1  48068  gpg3kgrtriexlem6  48092  gpgprismgr4cycllem3  48101  eenglngeehlnmlem2  48743