Theorem nsyl2 141

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)

Hypotheses

Ref	Expression
nsyl2.1	⊢ (𝜑 → ¬ 𝜓)
nsyl2.2	⊢ (¬ 𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl2	⊢ (𝜑 → 𝜒)

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl2.2	. . 3 ⊢ (¬ 𝜒 → 𝜓)
3	1, 2	nsyl3 138	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 114	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  con1i  147  oprcl  4898  epelg  5584  elfvdm  6942  ovrcl  7473  elfvov1  7474  elfvov2  7475  tfi  7875  limom  7904  oaabs2  8688  ecexr  8751  elpmi  8887  elmapex  8889  pmresg  8911  pmsspw  8918  ixpssmap2g  8968  ixpssmapg  8969  resixpfo  8977  infensuc  9196  pm54.43lem  10041  alephnbtwn  10112  cfpwsdom  10625  elbasfv  17254  elbasov  17255  restsspw  17477  homarcl  18074  isipodrs  18583  grpidval  18675  efgrelexlema  19768  subcmn  19856  dvdsrval  20362  elocv  21687  mvrf1  22007  pf1rcl  22354  matrcl  22417  restrcl  23166  ssrest  23185  iscnp2  23248  isfcls  24018  isnghm  24745  dchrrcl  27285  sltval2  27702  sltres  27708  clwwlknnn  30053  hmdmadj  31960  indispconn  35240  cvmtop1  35266  cvmtop2  35267  mrsub0  35522  mrsubf  35523  mrsubccat  35524  mrsubcn  35525  mrsubco  35527  mrsubvrs  35528  msubf  35538  mclsrcl  35567  dfon2lem7  35791  funpartlem  35944  rankeq1o  36173  bj-brrelex12ALT  37069  bj-fvimacnv0  37288  atbase  39291  llnbase  39512  lplnbase  39537  lvolbase  39581  lhpbase  40001  mapco2g  42730