Theorem nsyl2 145

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 143	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  4662  elfvdm  6478  ovrcl  6962  tfi  7331  limom  7358  oaabs2  8009  ecexr  8031  elpmi  8159  elmapex  8161  pmresg  8168  pmsspw  8175  ixpssmap2g  8223  ixpssmapg  8224  resixpfo  8232  infensuc  8426  pm54.43lem  9158  alephnbtwn  9227  cfpwsdom  9741  elbasfv  16316  elbasov  16317  restsspw  16478  homarcl  17063  isipodrs  17547  grpidval  17646  efgrelexlema  18548  subcmn  18628  dvdsrval  19032  mvrf1  19822  pf1rcl  20109  elocv  20411  matrcl  20622  restrcl  21369  ssrest  21388  iscnp2  21451  isfcls  22221  isnghm  22935  dchrrcl  25417  eleenn  26245  clwwlknnn  27422  hmdmadj  29371  indispconn  31815  cvmtop1  31841  cvmtop2  31842  mrsub0  32012  mrsubf  32013  mrsubccat  32014  mrsubcn  32015  mrsubco  32017  mrsubvrs  32018  msubf  32028  mclsrcl  32057  dfon2lem7  32282  sltval2  32398  sltres  32404  funpartlem  32638  rankeq1o  32867  atbase  35438  llnbase  35658  lplnbase  35683  lvolbase  35727  lhpbase  36147  mapco2g  38230