Theorem 3mix3d 1238

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

Syntax hints:   → wi 4   ∨ w3o 1036

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 197  df-or 385  df-3or 1038

This theorem is referenced by:  funtpgOLD  5943  elfiun  8336  nnnegz  11380  hashv01gt1  13133  lcmfunsnlem2lem2  15352  cshwshashlem1  15802  dyaddisjlem  23363  zabsle1  25021  btwncolg3  25452  btwnlng3  25516  frgr3vlem2  27138  3vfriswmgr  27142  frgrregorufr0  27188  noextendgt  31823  sltsolem1  31826  nodense  31842  fnwe2lem3  37622