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  4866  epelg  5542  elfvdm  6898  ovrcl  7431  elfvov1  7432  elfvov2  7433  tfi  7832  limom  7861  oaabs2  8616  ecexr  8679  elpmi  8822  elmapex  8824  pmresg  8846  pmsspw  8853  ixpssmap2g  8903  ixpssmapg  8904  resixpfo  8912  infensuc  9125  pm54.43lem  9960  alephnbtwn  10031  cfpwsdom  10544  elbasfv  17192  elbasov  17193  restsspw  17401  homarcl  17997  isipodrs  18503  grpidval  18595  efgrelexlema  19686  subcmn  19774  dvdsrval  20277  elocv  21584  mvrf1  21902  pf1rcl  22243  matrcl  22306  restrcl  23051  ssrest  23070  iscnp2  23133  isfcls  23903  isnghm  24618  dchrrcl  27158  sltval2  27575  sltres  27581  clwwlknnn  29969  hmdmadj  31876  indispconn  35228  cvmtop1  35254  cvmtop2  35255  mrsub0  35510  mrsubf  35511  mrsubccat  35512  mrsubcn  35513  mrsubco  35515  mrsubvrs  35516  msubf  35526  mclsrcl  35555  dfon2lem7  35784  funpartlem  35937  rankeq1o  36166  bj-brrelex12ALT  37062  bj-fvimacnv0  37281  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  lhpbase  39999  mapco2g  42709