Theorem 3mix2d 1338

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 1332	. 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  5710  f1dom3fv3dif  7209  f1dom3el3dif  7210  xpord3inddlem  8094  elfiun  9339  fpwwe2lem12  10555  fvf1tp  13712  swrdnd0  14583  lcmfunsnlem2lem2  16569  dyaddisjlem  25513  sltsolem1  27604  tgcolg  28518  btwncolg2  28520  hlln  28571  btwnlng2  28584  frgrregorufr0  30287  constrsslem  33727  constrlccllem  33739  colineartriv2  36061  gpgprismgriedgdmss  48056  gpgvtxedg0  48067  gpgvtxedg1  48068  gpgedgiov  48069  eenglngeehlnmlem2  48743