Theorem 3mix3d 1338

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 1332	. 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  8180  elfiun  9471  nnnegz  12618  fvf1tp  13830  hashv01gt1  14385  lcmfunsnlem2lem2  16677  cshwshashlem1  17134  dyaddisjlem  25631  zabsle1  27341  noextendgt  27716  sltsolem1  27721  nodense  27738  btwncolg3  28566  btwnlng3  28630  frgr3vlem2  30294  3vfriswmgr  30298  frgrregorufr0  30344  weiunso  36468  fnwe2lem3  43069  omcl2  43351  gpgedgvtx1  48025  gpgvtxedg0  48026  gpgvtxedg1  48027  gpg3kgrtriexlem6  48049  eenglngeehlnmlem2  48664