Theorem nsyl2 143

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 140	. 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  149  oprcl  4791  epelg  5431  elfvdm  6677  ovrcl  7176  tfi  7548  limom  7575  oaabs2  8255  ecexr  8277  elpmi  8408  elmapex  8410  pmresg  8417  pmsspw  8424  ixpssmap2g  8474  ixpssmapg  8475  resixpfo  8483  infensuc  8679  pm54.43lem  9413  alephnbtwn  9482  cfpwsdom  9995  elbasfv  16536  elbasov  16537  restsspw  16697  homarcl  17280  isipodrs  17763  grpidval  17863  efgrelexlema  18867  subcmn  18950  dvdsrval  19391  elocv  20357  mvrf1  20663  pf1rcl  20973  matrcl  21017  restrcl  21762  ssrest  21781  iscnp2  21844  isfcls  22614  isnghm  23329  dchrrcl  25824  clwwlknnn  27818  hmdmadj  29723  indispconn  32594  cvmtop1  32620  cvmtop2  32621  mrsub0  32876  mrsubf  32877  mrsubccat  32878  mrsubcn  32879  mrsubco  32881  mrsubvrs  32882  msubf  32892  mclsrcl  32921  dfon2lem7  33147  sltval2  33276  sltres  33282  funpartlem  33516  rankeq1o  33745  bj-brrelex12ALT  34483  bj-fvimacnv0  34701  atbase  36585  llnbase  36805  lplnbase  36830  lvolbase  36874  lhpbase  37294  mapco2g  39655