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  4459  ovrcl  6726  tfi  7095  limom  7122  oaabs2  7770  ecexr  7792  elpmi  7918  elmapex  7920  pmresg  7927  pmsspw  7934  ixpssmap2g  7979  ixpssmapg  7980  resixpfo  7988  infensuc  8179  pm54.43lem  8863  alephnbtwn  8932  cfpwsdom  9444  elbasfv  15967  elbasov  15968  restsspw  16139  homarcl  16725  isipodrs  17208  grpidval  17307  efgrelexlema  18208  subcmn  18288  dvdsrval  18691  mvrf1  19473  pf1rcl  19761  elocv  20060  matrcl  20266  restrcl  21009  ssrest  21028  iscnp2  21091  isfcls  21860  isnghm  22574  dchrrcl  25010  eleenn  25821  clwwlknnn  26995  hmdmadj  28927  indispconn  31342  cvmtop1  31368  cvmtop2  31369  mrsub0  31539  mrsubf  31540  mrsubccat  31541  mrsubcn  31542  mrsubco  31544  mrsubvrs  31545  msubf  31555  mclsrcl  31584  dfon2lem7  31818  sltval2  31934  sltres  31940  funpartlem  32174  rankeq1o  32403  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  lhpbase  35602  mapco2g  37594