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  4830  epelg  5519  elfvdm  6861  ovrcl  7397  elfvov1  7398  elfvov2  7399  tfi  7793  limom  7822  oaabs2  8575  ecexr  8638  elpmi  8783  elmapex  8785  pmresg  8808  pmsspw  8815  ixpssmap2g  8865  ixpssmapg  8866  resixpfo  8874  infensuc  9083  pm54.43lem  9915  alephnbtwn  9984  cfpwsdom  10498  elbasfv  17176  elbasov  17177  restsspw  17385  homarcl  17986  isipodrs  18494  grpidval  18620  efgrelexlema  19715  subcmn  19803  dvdsrval  20332  elocv  21643  mvrf1  21960  pf1rcl  22335  matrcl  22395  restrcl  23140  ssrest  23159  iscnp2  23222  isfcls  23992  isnghm  24706  dchrrcl  27221  ltsval2  27638  ltsres  27644  clwwlknnn  30121  hmdmadj  32029  indispconn  35462  cvmtop1  35488  cvmtop2  35489  mrsub0  35744  mrsubf  35745  mrsubccat  35746  mrsubcn  35747  mrsubco  35749  mrsubvrs  35750  msubf  35760  mclsrcl  35789  dfon2lem7  36015  funpartlem  36170  rankeq1o  36399  bj-brrelex12ALT  37420  bj-fvimacnv0  37646  atbase  39781  llnbase  40001  lplnbase  40026  lvolbase  40070  lhpbase  40490  mapco2g  43163