Theorem 3mix3d 1231

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 1225	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ w3o 1030

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 196  df-or 384  df-3or 1032

This theorem is referenced by:  funtpgOLD  5857  elfiun  8219  nnnegz  11257  hashv01gt1  12995  lcmfunsnlem2lem2  15190  cshwshashlem1  15640  dyaddisjlem  23169  zabsle1  24821  btwncolg3  25252  btwnlng3  25316  frgra3vlem2  26528  3vfriswmgra  26532  frgraregorufr0  26579  2spotdisj  26588  sltsolem1  31067  nodense  31088  fnwe2lem3  36640  frgr3vlem2  41444  3vfriswmgr  41448  frgrregorufr0  41489