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  4900  epelg  5582  elfvdm  6929  ovrcl  7454  tfi  7846  limom  7875  oaabs2  8652  ecexr  8712  elpmi  8844  elmapex  8846  pmresg  8868  pmsspw  8875  ixpssmap2g  8925  ixpssmapg  8926  resixpfo  8934  infensuc  9159  pm54.43lem  9999  alephnbtwn  10070  cfpwsdom  10583  elbasfv  17156  elbasov  17157  restsspw  17383  homarcl  17984  isipodrs  18496  grpidval  18588  efgrelexlema  19660  subcmn  19748  dvdsrval  20254  elocv  21442  mvrf1  21766  pf1rcl  22090  matrcl  22134  restrcl  22883  ssrest  22902  iscnp2  22965  isfcls  23735  isnghm  24462  dchrrcl  26977  sltval2  27393  sltres  27399  clwwlknnn  29551  hmdmadj  31458  indispconn  34521  cvmtop1  34547  cvmtop2  34548  mrsub0  34803  mrsubf  34804  mrsubccat  34805  mrsubcn  34806  mrsubco  34808  mrsubvrs  34809  msubf  34819  mclsrcl  34848  dfon2lem7  35063  funpartlem  35216  rankeq1o  35445  bj-brrelex12ALT  36253  bj-fvimacnv0  36472  atbase  38464  llnbase  38685  lplnbase  38710  lvolbase  38754  lhpbase  39174  mapco2g  41756