Theorem 3mix3d 1336

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

Syntax hints:   → wi 4   ∨ w3o 1084

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

This theorem is referenced by:  elfiun  9119  nnnegz  12252  hashv01gt1  13987  lcmfunsnlem2lem2  16272  cshwshashlem1  16725  dyaddisjlem  24664  zabsle1  26349  btwncolg3  26822  btwnlng3  26886  frgr3vlem2  28539  3vfriswmgr  28543  frgrregorufr0  28589  xpord3ind  33727  noextendgt  33800  sltsolem1  33805  nodense  33822  fnwe2lem3  40793  eenglngeehlnmlem2  45972