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  4853  epelg  5524  elfvdm  6861  ovrcl  7394  elfvov1  7395  elfvov2  7396  tfi  7793  limom  7822  oaabs2  8574  ecexr  8637  elpmi  8780  elmapex  8782  pmresg  8804  pmsspw  8811  ixpssmap2g  8861  ixpssmapg  8862  resixpfo  8870  infensuc  9079  pm54.43lem  9915  alephnbtwn  9984  cfpwsdom  10497  elbasfv  17145  elbasov  17146  restsspw  17354  homarcl  17954  isipodrs  18462  grpidval  18554  efgrelexlema  19647  subcmn  19735  dvdsrval  20265  elocv  21594  mvrf1  21912  pf1rcl  22253  matrcl  22316  restrcl  23061  ssrest  23080  iscnp2  23143  isfcls  23913  isnghm  24628  dchrrcl  27168  sltval2  27585  sltres  27591  clwwlknnn  29996  hmdmadj  31903  indispconn  35226  cvmtop1  35252  cvmtop2  35253  mrsub0  35508  mrsubf  35509  mrsubccat  35510  mrsubcn  35511  mrsubco  35513  mrsubvrs  35514  msubf  35524  mclsrcl  35553  dfon2lem7  35782  funpartlem  35935  rankeq1o  36164  bj-brrelex12ALT  37060  bj-fvimacnv0  37279  atbase  39287  llnbase  39508  lplnbase  39533  lvolbase  39577  lhpbase  39997  mapco2g  42707