Theorem 3mix3d 1337

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 1331	. 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 206  df-or 845  df-3or 1087

This theorem is referenced by:  elfiun  9189  nnnegz  12322  hashv01gt1  14059  lcmfunsnlem2lem2  16344  cshwshashlem1  16797  dyaddisjlem  24759  zabsle1  26444  btwncolg3  26918  btwnlng3  26982  frgr3vlem2  28638  3vfriswmgr  28642  frgrregorufr0  28688  xpord3ind  33800  noextendgt  33873  sltsolem1  33878  nodense  33895  fnwe2lem3  40877  eenglngeehlnmlem2  46084