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  4904  epelg  5590  elfvdm  6944  ovrcl  7472  elfvov1  7473  elfvov2  7474  tfi  7874  limom  7903  oaabs2  8686  ecexr  8749  elpmi  8885  elmapex  8887  pmresg  8909  pmsspw  8916  ixpssmap2g  8966  ixpssmapg  8967  resixpfo  8975  infensuc  9194  pm54.43lem  10038  alephnbtwn  10109  cfpwsdom  10622  elbasfv  17251  elbasov  17252  restsspw  17478  homarcl  18082  isipodrs  18595  grpidval  18687  efgrelexlema  19782  subcmn  19870  dvdsrval  20378  elocv  21704  mvrf1  22024  pf1rcl  22369  matrcl  22432  restrcl  23181  ssrest  23200  iscnp2  23263  isfcls  24033  isnghm  24760  dchrrcl  27299  sltval2  27716  sltres  27722  clwwlknnn  30062  hmdmadj  31969  indispconn  35219  cvmtop1  35245  cvmtop2  35246  mrsub0  35501  mrsubf  35502  mrsubccat  35503  mrsubcn  35504  mrsubco  35506  mrsubvrs  35507  msubf  35517  mclsrcl  35546  dfon2lem7  35771  funpartlem  35924  rankeq1o  36153  bj-brrelex12ALT  37050  bj-fvimacnv0  37269  atbase  39271  llnbase  39492  lplnbase  39517  lvolbase  39561  lhpbase  39981  mapco2g  42702