Theorem nsyl2 143

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 140	. 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  149  oprcl  4829  epelg  5466  elfvdm  6702  ovrcl  7197  tfi  7568  limom  7595  oaabs2  8272  ecexr  8294  elpmi  8425  elmapex  8427  pmresg  8434  pmsspw  8441  ixpssmap2g  8491  ixpssmapg  8492  resixpfo  8500  infensuc  8695  pm54.43lem  9428  alephnbtwn  9497  cfpwsdom  10006  elbasfv  16544  elbasov  16545  restsspw  16705  homarcl  17288  isipodrs  17771  grpidval  17871  efgrelexlema  18875  subcmn  18957  dvdsrval  19395  mvrf1  20205  pf1rcl  20512  elocv  20812  matrcl  21021  restrcl  21765  ssrest  21784  iscnp2  21847  isfcls  22617  isnghm  23332  dchrrcl  25816  clwwlknnn  27811  hmdmadj  29717  indispconn  32481  cvmtop1  32507  cvmtop2  32508  mrsub0  32763  mrsubf  32764  mrsubccat  32765  mrsubcn  32766  mrsubco  32768  mrsubvrs  32769  msubf  32779  mclsrcl  32808  dfon2lem7  33034  sltval2  33163  sltres  33169  funpartlem  33403  rankeq1o  33632  bj-brrelex12ALT  34362  bj-fvimacnv0  34571  atbase  36440  llnbase  36660  lplnbase  36685  lvolbase  36729  lhpbase  37149  mapco2g  39360