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  4854  epelg  5544  elfvdm  6896  ovrcl  7432  elfvov1  7433  elfvov2  7434  tfi  7828  limom  7857  oaabs2  8613  ecexr  8677  elpmi  8821  elmapex  8823  pmresg  8846  pmsspw  8853  ixpssmap2g  8903  ixpssmapg  8904  resixpfo  8912  infensuc  9121  pm54.43lem  9952  alephnbtwn  10021  cfpwsdom  10536  elbasfv  17242  elbasov  17243  restsspw  17451  homarcl  18052  isipodrs  18560  grpidval  18686  efgrelexlema  19780  subcmn  19868  dvdsrval  20397  elocv  21708  mvrf1  22025  pf1rcl  22400  matrcl  22460  restrcl  23205  ssrest  23224  iscnp2  23287  isfcls  24057  isnghm  24771  dchrrcl  27292  ltsval2  27708  ltsres  27714  clwwlknnn  30192  hmdmadj  32100  indispconn  35545  cvmtop1  35571  cvmtop2  35572  mrsub0  35827  mrsubf  35828  mrsubccat  35829  mrsubcn  35830  mrsubco  35832  mrsubvrs  35833  msubf  35843  mclsrcl  35872  dfon2lem7  36098  funpartlem  36253  rankeq1o  36482  bj-brrelex12ALT  37513  bj-fvimacnv0  37739  atbase  39874  llnbase  40094  lplnbase  40119  lvolbase  40163  lhpbase  40583  mapco2g  43256