Theorem 3mix3d 1334

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 209  df-or 844  df-3or 1084

This theorem is referenced by:  elfiun  8888  nnnegz  11978  hashv01gt1  13699  lcmfunsnlem2lem2  15977  cshwshashlem1  16423  dyaddisjlem  24190  zabsle1  25866  btwncolg3  26337  btwnlng3  26401  frgr3vlem2  28047  3vfriswmgr  28051  frgrregorufr0  28097  noextendgt  33172  sltsolem1  33175  nodense  33191  fnwe2lem3  39645  eenglngeehlnmlem2  44719