Theorem 3mix3d 1337

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 1331	. 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  8178  elfiun  9468  nnnegz  12614  fvf1tp  13826  hashv01gt1  14381  lcmfunsnlem2lem2  16673  cshwshashlem1  17130  dyaddisjlem  25644  zabsle1  27355  noextendgt  27730  sltsolem1  27735  nodense  27752  btwncolg3  28580  btwnlng3  28644  frgr3vlem2  30303  3vfriswmgr  30307  frgrregorufr0  30353  weiunso  36449  fnwe2lem3  43041  omcl2  43323  gpgedgvtx1  47955  gpgvtxedg0  47956  gpgvtxedg1  47957  eenglngeehlnmlem2  48588