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  4831  epelg  5497  elfvdm  6815  ovrcl  7325  tfi  7709  limom  7737  oaabs2  8488  ecexr  8512  elpmi  8643  elmapex  8645  pmresg  8667  pmsspw  8674  ixpssmap2g  8724  ixpssmapg  8725  resixpfo  8733  infensuc  8951  pm54.43lem  9767  alephnbtwn  9836  cfpwsdom  10349  elbasfv  16927  elbasov  16928  restsspw  17151  homarcl  17752  isipodrs  18264  grpidval  18354  efgrelexlema  19364  subcmn  19447  dvdsrval  19896  elocv  20882  mvrf1  21203  pf1rcl  21524  matrcl  21568  restrcl  22317  ssrest  22336  iscnp2  22399  isfcls  23169  isnghm  23896  dchrrcl  26397  clwwlknnn  28406  hmdmadj  30311  indispconn  33205  cvmtop1  33231  cvmtop2  33232  mrsub0  33487  mrsubf  33488  mrsubccat  33489  mrsubcn  33490  mrsubco  33492  mrsubvrs  33493  msubf  33503  mclsrcl  33532  dfon2lem7  33774  sltval2  33868  sltres  33874  funpartlem  34253  rankeq1o  34482  bj-brrelex12ALT  35247  bj-fvimacnv0  35466  atbase  37310  llnbase  37530  lplnbase  37555  lvolbase  37599  lhpbase  38019  mapco2g  40543