Theorem 3mix2d 1333

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

Syntax hints:   → wi 4   ∨ w3o 1082

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

This theorem is referenced by:  sosn  5640  f1dom3fv3dif  7028  f1dom3el3dif  7029  elfiun  8896  fpwwe2lem13  10066  swrdnd0  14021  lcmfunsnlem2lem2  15985  dyaddisjlem  24198  tgcolg  26342  btwncolg2  26344  hlln  26395  btwnlng2  26408  frgrregorufr0  28105  sltsolem1  33182  colineartriv2  33531  eenglngeehlnmlem2  44732