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  5673  f1dom3fv3dif  7141  f1dom3el3dif  7142  elfiun  9189  fpwwe2lem12  10398  swrdnd0  14370  lcmfunsnlem2lem2  16344  dyaddisjlem  24759  tgcolg  26915  btwncolg2  26917  hlln  26968  btwnlng2  26981  frgrregorufr0  28688  xpord3ind  33800  sltsolem1  33878  colineartriv2  34370  eenglngeehlnmlem2  46084