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  4842  epelg  5532  elfvdm  6874  ovrcl  7408  elfvov1  7409  elfvov2  7410  tfi  7804  limom  7833  oaabs2  8585  ecexr  8648  elpmi  8793  elmapex  8795  pmresg  8818  pmsspw  8825  ixpssmap2g  8875  ixpssmapg  8876  resixpfo  8884  infensuc  9093  pm54.43lem  9924  alephnbtwn  9993  cfpwsdom  10507  elbasfv  17185  elbasov  17186  restsspw  17394  homarcl  17995  isipodrs  18503  grpidval  18629  efgrelexlema  19724  subcmn  19812  dvdsrval  20341  elocv  21648  mvrf1  21964  pf1rcl  22314  matrcl  22377  restrcl  23122  ssrest  23141  iscnp2  23204  isfcls  23974  isnghm  24688  dchrrcl  27203  ltsval2  27620  ltsres  27626  clwwlknnn  30103  hmdmadj  32011  indispconn  35416  cvmtop1  35442  cvmtop2  35443  mrsub0  35698  mrsubf  35699  mrsubccat  35700  mrsubcn  35701  mrsubco  35703  mrsubvrs  35704  msubf  35714  mclsrcl  35743  dfon2lem7  35969  funpartlem  36124  rankeq1o  36353  bj-brrelex12ALT  37374  bj-fvimacnv0  37600  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  lhpbase  40444  mapco2g  43146