Theorem 3mix2d 1337

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 1088

This theorem is referenced by:  sosn  5760  f1dom3fv3dif  7263  f1dom3el3dif  7264  xpord3inddlem  8136  elfiun  9421  fpwwe2lem12  10633  swrdnd0  14603  lcmfunsnlem2lem2  16572  dyaddisjlem  25103  sltsolem1  27167  tgcolg  27794  btwncolg2  27796  hlln  27847  btwnlng2  27860  frgrregorufr0  29566  colineartriv2  35028  eenglngeehlnmlem2  47377