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

This theorem is referenced by:  sosn  5774  f1dom3fv3dif  7287  f1dom3el3dif  7288  xpord3inddlem  8177  elfiun  9467  fpwwe2lem12  10679  fvf1tp  13825  swrdnd0  14691  lcmfunsnlem2lem2  16672  dyaddisjlem  25643  sltsolem1  27734  tgcolg  28576  btwncolg2  28578  hlln  28629  btwnlng2  28642  frgrregorufr0  30352  constrsslem  33745  colineartriv2  36049  gpgvtxedg0  47955  gpgvtxedg1  47956  eenglngeehlnmlem2  48587