Theorem 3mix3d 1335

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

Syntax hints:   → wi 4   ∨ w3o 1083

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 846  df-3or 1085

This theorem is referenced by:  xpord3inddlem  8168  elfiun  9473  nnnegz  12613  hashv01gt1  14362  lcmfunsnlem2lem2  16640  cshwshashlem1  17098  dyaddisjlem  25615  zabsle1  27325  noextendgt  27700  sltsolem1  27705  nodense  27722  btwncolg3  28484  btwnlng3  28548  frgr3vlem2  30207  3vfriswmgr  30211  frgrregorufr0  30257  fnwe2lem3  42713  omcl2  42999  eenglngeehlnmlem2  48126