Theorem nsyl2 144

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)

Hypotheses

Ref	Expression
nsyl2.1	⊢ (𝜑 → ¬ 𝜓)
nsyl2.2	⊢ (¬ 𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl2	⊢ (𝜑 → 𝜒)

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl2.2	. . 3 ⊢ (¬ 𝜒 → 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
4	1, 3	mt3d 142	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  146  oprcl  4566  ovrcl  6832  tfi  7201  limom  7228  oaabs2  7880  ecexr  7902  elpmi  8029  elmapex  8031  pmresg  8038  pmsspw  8045  ixpssmap2g  8092  ixpssmapg  8093  resixpfo  8101  infensuc  8295  pm54.43lem  9026  alephnbtwn  9095  cfpwsdom  9609  elbasfv  16128  elbasov  16129  restsspw  16301  homarcl  16886  isipodrs  17370  grpidval  17469  efgrelexlema  18370  subcmn  18450  dvdsrval  18854  mvrf1  19641  pf1rcl  19929  elocv  20230  matrcl  20436  restrcl  21183  ssrest  21202  iscnp2  21265  isfcls  22034  isnghm  22748  dchrrcl  25187  eleenn  25998  clwwlknnn  27189  hmdmadj  29140  indispconn  31555  cvmtop1  31581  cvmtop2  31582  mrsub0  31752  mrsubf  31753  mrsubccat  31754  mrsubcn  31755  mrsubco  31757  mrsubvrs  31758  msubf  31768  mclsrcl  31797  dfon2lem7  32031  sltval2  32147  sltres  32153  funpartlem  32387  rankeq1o  32616  atbase  35099  llnbase  35318  lplnbase  35343  lvolbase  35387  lhpbase  35807  mapco2g  37804