Theorem nsyl2 134

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 132	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  136  con4i  137  oprcl  4221  ovrcl  6397  tfi  6757  limom  6784  oaabs2  7423  ecexr  7445  elpmi  7573  elmapex  7575  pmresg  7582  pmsspw  7589  ixpssmap2g  7634  ixpssmapg  7635  resixpfo  7643  infensuc  7834  pm54.43lem  8518  alephnbtwn  8587  cfpwsdom  9094  elbasfv  15335  elbasov  15336  restsspw  15495  homarcl  16089  isipodrs  16572  grpidval  16668  efgrelexlema  17560  subcmn  17638  dvdsrval  18033  mvrf1  18808  pf1rcl  19095  elocv  19389  matrcl  19595  restrcl  20330  ssrest  20349  iscnp2  20412  isfcls  21182  isnghm  21886  isnghmOLD  21904  dchrrcl  24329  eleenn  25087  hmdmadj  27756  indispcon  30109  cvmtop1  30135  cvmtop2  30136  mrsub0  30306  mrsubf  30307  mrsubccat  30308  mrsubcn  30309  mrsubco  30311  mrsubvrs  30312  msubf  30322  mclsrcl  30351  dfon2lem7  30586  sltval2  30694  sltres  30702  funpartlem  30860  rankeq1o  31089  atbase  33095  llnbase  33314  lplnbase  33339  lvolbase  33383  lhpbase  33803  mapco2g  35796