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  8079  elfiun  9309  nnnegz  12466  fvf1tp  13688  hashv01gt1  14247  lcmfunsnlem2lem2  16545  cshwshashlem1  17002  dyaddisjlem  25518  zabsle1  27229  noextendgt  27604  sltsolem1  27609  nodense  27626  btwncolg3  28530  btwnlng3  28594  frgr3vlem2  30246  3vfriswmgr  30250  frgrregorufr0  30296  constrcccllem  33759  weiunso  36500  fnwe2lem3  43085  omcl2  43366  gpgprismgriedgdmss  48083  gpgedgvtx1  48093  gpgvtxedg0  48094  gpgvtxedg1  48095  gpg3kgrtriexlem6  48119  gpgprismgr4cycllem3  48128  eenglngeehlnmlem2  48770