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  4855  epelg  5525  elfvdm  6868  ovrcl  7399  elfvov1  7400  elfvov2  7401  tfi  7795  limom  7824  oaabs2  8577  ecexr  8640  elpmi  8783  elmapex  8785  pmresg  8808  pmsspw  8815  ixpssmap2g  8865  ixpssmapg  8866  resixpfo  8874  infensuc  9083  pm54.43lem  9912  alephnbtwn  9981  cfpwsdom  10495  elbasfv  17142  elbasov  17143  restsspw  17351  homarcl  17952  isipodrs  18460  grpidval  18586  efgrelexlema  19678  subcmn  19766  dvdsrval  20297  elocv  21623  mvrf1  21941  pf1rcl  22293  matrcl  22356  restrcl  23101  ssrest  23120  iscnp2  23183  isfcls  23953  isnghm  24667  dchrrcl  27207  ltsval2  27624  ltsres  27630  clwwlknnn  30108  hmdmadj  32015  indispconn  35428  cvmtop1  35454  cvmtop2  35455  mrsub0  35710  mrsubf  35711  mrsubccat  35712  mrsubcn  35713  mrsubco  35715  mrsubvrs  35716  msubf  35726  mclsrcl  35755  dfon2lem7  35981  funpartlem  36136  rankeq1o  36365  bj-brrelex12ALT  37268  bj-fvimacnv0  37491  atbase  39549  llnbase  39769  lplnbase  39794  lvolbase  39838  lhpbase  40258  mapco2g  42956