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  4846  epelg  5512  elfvdm  6851  ovrcl  7382  elfvov1  7383  elfvov2  7384  tfi  7778  limom  7807  oaabs2  8559  ecexr  8622  elpmi  8765  elmapex  8767  pmresg  8789  pmsspw  8796  ixpssmap2g  8846  ixpssmapg  8847  resixpfo  8855  infensuc  9063  pm54.43lem  9888  alephnbtwn  9957  cfpwsdom  10470  elbasfv  17121  elbasov  17122  restsspw  17330  homarcl  17930  isipodrs  18438  grpidval  18564  efgrelexlema  19656  subcmn  19744  dvdsrval  20274  elocv  21600  mvrf1  21918  pf1rcl  22259  matrcl  22322  restrcl  23067  ssrest  23086  iscnp2  23149  isfcls  23919  isnghm  24633  dchrrcl  27173  sltval2  27590  sltres  27596  clwwlknnn  30005  hmdmadj  31912  indispconn  35270  cvmtop1  35296  cvmtop2  35297  mrsub0  35552  mrsubf  35553  mrsubccat  35554  mrsubcn  35555  mrsubco  35557  mrsubvrs  35558  msubf  35568  mclsrcl  35597  dfon2lem7  35823  funpartlem  35976  rankeq1o  36205  bj-brrelex12ALT  37101  bj-fvimacnv0  37320  atbase  39328  llnbase  39548  lplnbase  39573  lvolbase  39617  lhpbase  40037  mapco2g  42747