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  4852  epelg  5522  elfvdm  6865  ovrcl  7396  elfvov1  7397  elfvov2  7398  tfi  7792  limom  7821  oaabs2  8573  ecexr  8636  elpmi  8779  elmapex  8781  pmresg  8804  pmsspw  8811  ixpssmap2g  8861  ixpssmapg  8862  resixpfo  8870  infensuc  9079  pm54.43lem  9904  alephnbtwn  9973  cfpwsdom  10486  elbasfv  17133  elbasov  17134  restsspw  17342  homarcl  17943  isipodrs  18451  grpidval  18577  efgrelexlema  19669  subcmn  19757  dvdsrval  20288  elocv  21614  mvrf1  21932  pf1rcl  22284  matrcl  22347  restrcl  23092  ssrest  23111  iscnp2  23174  isfcls  23944  isnghm  24658  dchrrcl  27198  sltval2  27615  sltres  27621  clwwlknnn  30034  hmdmadj  31941  indispconn  35350  cvmtop1  35376  cvmtop2  35377  mrsub0  35632  mrsubf  35633  mrsubccat  35634  mrsubcn  35635  mrsubco  35637  mrsubvrs  35638  msubf  35648  mclsrcl  35677  dfon2lem7  35903  funpartlem  36058  rankeq1o  36287  bj-brrelex12ALT  37184  bj-fvimacnv0  37403  atbase  39461  llnbase  39681  lplnbase  39706  lvolbase  39750  lhpbase  40170  mapco2g  42871