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  4859  epelg  5532  elfvdm  6877  ovrcl  7410  elfvov1  7411  elfvov2  7412  tfi  7809  limom  7838  oaabs2  8590  ecexr  8653  elpmi  8796  elmapex  8798  pmresg  8820  pmsspw  8827  ixpssmap2g  8877  ixpssmapg  8878  resixpfo  8886  infensuc  9096  pm54.43lem  9929  alephnbtwn  10000  cfpwsdom  10513  elbasfv  17161  elbasov  17162  restsspw  17370  homarcl  17966  isipodrs  18472  grpidval  18564  efgrelexlema  19655  subcmn  19743  dvdsrval  20246  elocv  21553  mvrf1  21871  pf1rcl  22212  matrcl  22275  restrcl  23020  ssrest  23039  iscnp2  23102  isfcls  23872  isnghm  24587  dchrrcl  27127  sltval2  27544  sltres  27550  clwwlknnn  29935  hmdmadj  31842  indispconn  35194  cvmtop1  35220  cvmtop2  35221  mrsub0  35476  mrsubf  35477  mrsubccat  35478  mrsubcn  35479  mrsubco  35481  mrsubvrs  35482  msubf  35492  mclsrcl  35521  dfon2lem7  35750  funpartlem  35903  rankeq1o  36132  bj-brrelex12ALT  37028  bj-fvimacnv0  37247  atbase  39255  llnbase  39476  lplnbase  39501  lvolbase  39545  lhpbase  39965  mapco2g  42675