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  4923  epelg  5600  elfvdm  6957  ovrcl  7489  elfvov1  7490  elfvov2  7491  tfi  7890  limom  7919  oaabs2  8705  ecexr  8768  elpmi  8904  elmapex  8906  pmresg  8928  pmsspw  8935  ixpssmap2g  8985  ixpssmapg  8986  resixpfo  8994  infensuc  9221  pm54.43lem  10069  alephnbtwn  10140  cfpwsdom  10653  elbasfv  17264  elbasov  17265  restsspw  17491  homarcl  18095  isipodrs  18607  grpidval  18699  efgrelexlema  19791  subcmn  19879  dvdsrval  20387  elocv  21709  mvrf1  22029  pf1rcl  22374  matrcl  22437  restrcl  23186  ssrest  23205  iscnp2  23268  isfcls  24038  isnghm  24765  dchrrcl  27302  sltval2  27719  sltres  27725  clwwlknnn  30065  hmdmadj  31972  indispconn  35202  cvmtop1  35228  cvmtop2  35229  mrsub0  35484  mrsubf  35485  mrsubccat  35486  mrsubcn  35487  mrsubco  35489  mrsubvrs  35490  msubf  35500  mclsrcl  35529  dfon2lem7  35753  funpartlem  35906  rankeq1o  36135  bj-brrelex12ALT  37033  bj-fvimacnv0  37252  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  lhpbase  39955  mapco2g  42670