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  8096  elfiun  9333  nnnegz  12491  fvf1tp  13709  hashv01gt1  14268  lcmfunsnlem2lem2  16566  cshwshashlem1  17023  dyaddisjlem  25552  zabsle1  27263  noextendgt  27638  ltssolem1  27643  nodense  27660  btwncolg3  28629  btwnlng3  28693  frgr3vlem2  30349  3vfriswmgr  30353  frgrregorufr0  30399  constrcccllem  33911  weiunso  36660  fnwe2lem3  43294  omcl2  43575  gpgprismgriedgdmss  48298  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpg3kgrtriexlem6  48334  gpgprismgr4cycllem3  48343  eenglngeehlnmlem2  48984