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  4843  epelg  5525  elfvdm  6868  ovrcl  7401  elfvov1  7402  elfvov2  7403  tfi  7797  limom  7826  oaabs2  8578  ecexr  8641  elpmi  8786  elmapex  8788  pmresg  8811  pmsspw  8818  ixpssmap2g  8868  ixpssmapg  8869  resixpfo  8877  infensuc  9086  pm54.43lem  9915  alephnbtwn  9984  cfpwsdom  10498  elbasfv  17176  elbasov  17177  restsspw  17385  homarcl  17986  isipodrs  18494  grpidval  18620  efgrelexlema  19715  subcmn  19803  dvdsrval  20332  elocv  21658  mvrf1  21974  pf1rcl  22324  matrcl  22387  restrcl  23132  ssrest  23151  iscnp2  23214  isfcls  23984  isnghm  24698  dchrrcl  27217  ltsval2  27634  ltsres  27640  clwwlknnn  30118  hmdmadj  32026  indispconn  35432  cvmtop1  35458  cvmtop2  35459  mrsub0  35714  mrsubf  35715  mrsubccat  35716  mrsubcn  35717  mrsubco  35719  mrsubvrs  35720  msubf  35730  mclsrcl  35759  dfon2lem7  35985  funpartlem  36140  rankeq1o  36369  bj-brrelex12ALT  37390  bj-fvimacnv0  37616  atbase  39749  llnbase  39969  lplnbase  39994  lvolbase  40038  lhpbase  40458  mapco2g  43160