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  5728  f1dom3fv3dif  7246  f1dom3el3dif  7247  xpord3inddlem  8136  elfiun  9388  fpwwe2lem12  10602  fvf1tp  13758  swrdnd0  14629  lcmfunsnlem2lem2  16616  dyaddisjlem  25503  sltsolem1  27594  tgcolg  28488  btwncolg2  28490  hlln  28541  btwnlng2  28554  frgrregorufr0  30260  constrsslem  33738  constrlccllem  33750  colineartriv2  36063  gpgprismgriedgdmss  48047  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  eenglngeehlnmlem2  48731