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  4827  epelg  5487  elfvdm  6788  ovrcl  7296  tfi  7675  limom  7703  oaabs2  8439  ecexr  8461  elpmi  8592  elmapex  8594  pmresg  8616  pmsspw  8623  ixpssmap2g  8673  ixpssmapg  8674  resixpfo  8682  infensuc  8891  pm54.43lem  9689  alephnbtwn  9758  cfpwsdom  10271  elbasfv  16846  elbasov  16847  restsspw  17059  homarcl  17659  isipodrs  18170  grpidval  18260  efgrelexlema  19270  subcmn  19353  dvdsrval  19802  elocv  20785  mvrf1  21104  pf1rcl  21425  matrcl  21469  restrcl  22216  ssrest  22235  iscnp2  22298  isfcls  23068  isnghm  23793  dchrrcl  26293  clwwlknnn  28298  hmdmadj  30203  indispconn  33096  cvmtop1  33122  cvmtop2  33123  mrsub0  33378  mrsubf  33379  mrsubccat  33380  mrsubcn  33381  mrsubco  33383  mrsubvrs  33384  msubf  33394  mclsrcl  33423  dfon2lem7  33671  sltval2  33786  sltres  33792  funpartlem  34171  rankeq1o  34400  bj-brrelex12ALT  35165  bj-fvimacnv0  35384  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  lhpbase  37939  mapco2g  40452