Theorem nsyl2 142

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 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	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  148  oprcl  4865  epelg  5564  elfvdm  6917  ovrcl  7453  elfvov1  7454  elfvov2  7455  tfi  7850  limom  7879  oaabs2  8636  ecexr  8700  elpmi  8844  elmapex  8846  pmresg  8869  pmsspw  8876  ixpssmap2g  8926  ixpssmapg  8927  resixpfo  8935  infensuc  9144  pm54.43lem  9987  alephnbtwn  10056  cfpwsdom  10570  elbasfv  17276  elbasov  17277  restsspw  17485  homarcl  18086  isipodrs  18594  grpidval  18720  efgrelexlema  19820  subcmn  19908  dvdsrval  20444  elocv  21799  mvrf1  22116  pf1rcl  22490  matrcl  22550  restrcl  23295  ssrest  23314  iscnp2  23377  isfcls  24147  isnghm  24861  dchrrcl  27385  ltsval2  27801  ltsres  27807  clwwlknnn  30365  hmdmadj  32273  indispconn  35707  cvmtop1  35733  cvmtop2  35734  mrsub0  35989  mrsubf  35990  mrsubccat  35991  mrsubcn  35992  mrsubco  35994  mrsubvrs  35995  msubf  36005  mclsrcl  36034  dfon2lem7  36260  funpartlem  36415  rankeq1o  36644  bj-brrelex12ALT  37684  bj-fvimacnv0  37911  atbase  40044  llnbase  40264  lplnbase  40289  lvolbase  40333  lhpbase  40753  mapco2g  43428