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  4863  epelg  5539  elfvdm  6895  ovrcl  7428  elfvov1  7429  elfvov2  7430  tfi  7829  limom  7858  oaabs2  8613  ecexr  8676  elpmi  8819  elmapex  8821  pmresg  8843  pmsspw  8850  ixpssmap2g  8900  ixpssmapg  8901  resixpfo  8909  infensuc  9119  pm54.43lem  9953  alephnbtwn  10024  cfpwsdom  10537  elbasfv  17185  elbasov  17186  restsspw  17394  homarcl  17990  isipodrs  18496  grpidval  18588  efgrelexlema  19679  subcmn  19767  dvdsrval  20270  elocv  21577  mvrf1  21895  pf1rcl  22236  matrcl  22299  restrcl  23044  ssrest  23063  iscnp2  23126  isfcls  23896  isnghm  24611  dchrrcl  27151  sltval2  27568  sltres  27574  clwwlknnn  29962  hmdmadj  31869  indispconn  35221  cvmtop1  35247  cvmtop2  35248  mrsub0  35503  mrsubf  35504  mrsubccat  35505  mrsubcn  35506  mrsubco  35508  mrsubvrs  35509  msubf  35519  mclsrcl  35548  dfon2lem7  35777  funpartlem  35930  rankeq1o  36159  bj-brrelex12ALT  37055  bj-fvimacnv0  37274  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  lhpbase  39992  mapco2g  42702