Theorem nsyl2 142

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 140	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  144  con4iOLD  145  oprcl  4400  ovrcl  6640  tfi  7001  limom  7028  oaabs2  7671  ecexr  7693  elpmi  7821  elmapex  7823  pmresg  7830  pmsspw  7837  ixpssmap2g  7882  ixpssmapg  7883  resixpfo  7891  infensuc  8083  pm54.43lem  8770  alephnbtwn  8839  cfpwsdom  9351  elbasfv  15836  elbasov  15837  restsspw  16008  homarcl  16594  isipodrs  17077  grpidval  17176  efgrelexlema  18078  subcmn  18158  dvdsrval  18561  mvrf1  19339  pf1rcl  19627  elocv  19926  matrcl  20132  restrcl  20866  ssrest  20885  iscnp2  20948  isfcls  21718  isnghm  22432  dchrrcl  24860  eleenn  25671  hmdmadj  28639  indispconn  30916  cvmtop1  30942  cvmtop2  30943  mrsub0  31113  mrsubf  31114  mrsubccat  31115  mrsubcn  31116  mrsubco  31118  mrsubvrs  31119  msubf  31129  mclsrcl  31158  dfon2lem7  31383  sltval2  31498  sltres  31506  funpartlem  31664  rankeq1o  31893  atbase  34023  llnbase  34242  lplnbase  34267  lvolbase  34311  lhpbase  34731  mapco2g  36724