Theorem 3mix3d 1339

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

Syntax hints:   → wi 4   ∨ w3o 1087

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 847  df-3or 1089

This theorem is referenced by:  xpord3inddlem  8140  elfiun  9425  nnnegz  12561  hashv01gt1  14305  lcmfunsnlem2lem2  16576  cshwshashlem1  17029  dyaddisjlem  25112  zabsle1  26799  noextendgt  27173  sltsolem1  27178  nodense  27195  btwncolg3  27808  btwnlng3  27872  frgr3vlem2  29527  3vfriswmgr  29531  frgrregorufr0  29577  fnwe2lem3  41794  omcl2  42083  eenglngeehlnmlem2  47424