Theorem nsyl2 142

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 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	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  148  oprcl  4865  epelg  5560  elfvdm  6913  ovrcl  7449  elfvov1  7450  elfvov2  7451  tfi  7845  limom  7874  oaabs2  8631  ecexr  8695  elpmi  8839  elmapex  8841  pmresg  8864  pmsspw  8871  ixpssmap2g  8921  ixpssmapg  8922  resixpfo  8930  infensuc  9139  pm54.43lem  9982  alephnbtwn  10051  cfpwsdom  10565  elbasfv  17271  elbasov  17272  restsspw  17480  homarcl  18081  isipodrs  18589  grpidval  18715  efgrelexlema  19815  subcmn  19903  dvdsrval  20439  elocv  21783  mvrf1  22100  pf1rcl  22474  matrcl  22534  restrcl  23279  ssrest  23298  iscnp2  23361  isfcls  24131  isnghm  24845  dchrrcl  27366  ltsval2  27782  ltsres  27788  clwwlknnn  30321  hmdmadj  32229  indispconn  35621  cvmtop1  35647  cvmtop2  35648  mrsub0  35903  mrsubf  35904  mrsubccat  35905  mrsubcn  35906  mrsubco  35908  mrsubvrs  35909  msubf  35919  mclsrcl  35948  dfon2lem7  36174  funpartlem  36329  rankeq1o  36558  bj-brrelex12ALT  37587  bj-fvimacnv0  37813  atbase  39948  llnbase  40168  lplnbase  40193  lvolbase  40237  lhpbase  40657  mapco2g  43330