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  4857  epelg  5533  elfvdm  6876  ovrcl  7409  elfvov1  7410  elfvov2  7411  tfi  7805  limom  7834  oaabs2  8587  ecexr  8650  elpmi  8795  elmapex  8797  pmresg  8820  pmsspw  8827  ixpssmap2g  8877  ixpssmapg  8878  resixpfo  8886  infensuc  9095  pm54.43lem  9924  alephnbtwn  9993  cfpwsdom  10507  elbasfv  17154  elbasov  17155  restsspw  17363  homarcl  17964  isipodrs  18472  grpidval  18598  efgrelexlema  19690  subcmn  19778  dvdsrval  20309  elocv  21635  mvrf1  21953  pf1rcl  22305  matrcl  22368  restrcl  23113  ssrest  23132  iscnp2  23195  isfcls  23965  isnghm  24679  dchrrcl  27219  ltsval2  27636  ltsres  27642  clwwlknnn  30120  hmdmadj  32027  indispconn  35447  cvmtop1  35473  cvmtop2  35474  mrsub0  35729  mrsubf  35730  mrsubccat  35731  mrsubcn  35732  mrsubco  35734  mrsubvrs  35735  msubf  35745  mclsrcl  35774  dfon2lem7  36000  funpartlem  36155  rankeq1o  36384  bj-brrelex12ALT  37312  bj-fvimacnv0  37538  atbase  39662  llnbase  39882  lplnbase  39907  lvolbase  39951  lhpbase  40371  mapco2g  43068