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  4900  epelg  5582  elfvdm  6929  ovrcl  7450  tfi  7842  limom  7871  oaabs2  8648  ecexr  8708  elpmi  8840  elmapex  8842  pmresg  8864  pmsspw  8871  ixpssmap2g  8921  ixpssmapg  8922  resixpfo  8930  infensuc  9155  pm54.43lem  9995  alephnbtwn  10066  cfpwsdom  10579  elbasfv  17150  elbasov  17151  restsspw  17377  homarcl  17978  isipodrs  18490  grpidval  18580  efgrelexlema  19617  subcmn  19705  dvdsrval  20175  elocv  21221  mvrf1  21545  pf1rcl  21868  matrcl  21912  restrcl  22661  ssrest  22680  iscnp2  22743  isfcls  23513  isnghm  24240  dchrrcl  26743  sltval2  27159  sltres  27165  clwwlknnn  29286  hmdmadj  31193  indispconn  34225  cvmtop1  34251  cvmtop2  34252  mrsub0  34507  mrsubf  34508  mrsubccat  34509  mrsubcn  34510  mrsubco  34512  mrsubvrs  34513  msubf  34523  mclsrcl  34552  dfon2lem7  34761  funpartlem  34914  rankeq1o  35143  bj-brrelex12ALT  35948  bj-fvimacnv0  36167  atbase  38159  llnbase  38380  lplnbase  38405  lvolbase  38449  lhpbase  38869  mapco2g  41452