Theorem 3mix2d 1339

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix2d	⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Proof of Theorem 3mix2d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix2 1333	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1088

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 210  df-or 848  df-3or 1090

This theorem is referenced by:  sosn  5620  f1dom3fv3dif  7058  f1dom3el3dif  7059  elfiun  9024  fpwwe2lem12  10221  swrdnd0  14187  lcmfunsnlem2lem2  16159  dyaddisjlem  24446  tgcolg  26599  btwncolg2  26601  hlln  26652  btwnlng2  26665  frgrregorufr0  28361  xpord3ind  33480  sltsolem1  33564  colineartriv2  34056  eenglngeehlnmlem2  45700