Theorem nsyl2 142

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 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con1i  148  oprcl  4856  epelg  5551  elfvdm  6920  ovrcl  7462  elfvov1  7463  elfvov2  7464  tfi  7865  limom  7894  oaabs2  8662  ecexr  8726  elpmi  8870  elmapex  8872  pmresg  8902  pmsspw  8909  ixpssmap2g  8959  ixpssmapg  8960  resixpfo  8968  infensuc  9178  pm54.43lem  10085  alephnbtwn  10154  cfpwsdom  10673  elbasfv  17399  elbasov  17400  restsspw  17608  homarcl  18209  isipodrs  18717  grpidval  18846  efgrelexlema  19969  subcmn  20057  dvdsrval  20597  elocv  21980  mvrf1  22299  pf1rcl  22673  matrcl  22733  restrcl  23481  ssrest  23500  iscnp2  23563  isfcls  24334  isnghm  25048  dchrrcl  27573  ltsval2  28019  ltsres  28025  clwwlknnn  30630  hmdmadj  32548  indispconn  36086  cvmtop1  36112  cvmtop2  36113  mrsub0  36368  mrsubf  36369  mrsubccat  36370  mrsubcn  36371  mrsubco  36373  mrsubvrs  36374  msubf  36384  mclsrcl  36413  dfon2lem7  36644  funpartlem  36799  rankeq1o  37025  bj-brrelex12ALT  38075  bj-fvimacnv0  38301  atbase  40440  llnbase  40660  lplnbase  40685  lvolbase  40729  lhpbase  41149  mapco2g  43819