Theorem 3mix2d 1336

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 845  df-3or 1087

This theorem is referenced by:  sosn  5674  f1dom3fv3dif  7138  f1dom3el3dif  7139  elfiun  9177  fpwwe2lem12  10409  swrdnd0  14381  lcmfunsnlem2lem2  16355  dyaddisjlem  24770  tgcolg  26926  btwncolg2  26928  hlln  26979  btwnlng2  26992  frgrregorufr0  28697  xpord3ind  33809  sltsolem1  33887  colineartriv2  34379  eenglngeehlnmlem2  46063