Theorem nsyl2 141

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 139	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  143  con4iOLD  144  oprcl  4365  ovrcl  6584  tfi  6945  limom  6972  oaabs2  7612  ecexr  7634  elpmi  7762  elmapex  7764  pmresg  7771  pmsspw  7778  ixpssmap2g  7823  ixpssmapg  7824  resixpfo  7832  infensuc  8023  pm54.43lem  8708  alephnbtwn  8777  cfpwsdom  9285  elbasfv  15748  elbasov  15749  restsspw  15915  homarcl  16501  isipodrs  16984  grpidval  17083  efgrelexlema  17985  subcmn  18065  dvdsrval  18468  mvrf1  19246  pf1rcl  19534  elocv  19831  matrcl  20037  restrcl  20771  ssrest  20790  iscnp2  20853  isfcls  21623  isnghm  22337  dchrrcl  24765  eleenn  25576  hmdmadj  28183  indispcon  30470  cvmtop1  30496  cvmtop2  30497  mrsub0  30667  mrsubf  30668  mrsubccat  30669  mrsubcn  30670  mrsubco  30672  mrsubvrs  30673  msubf  30683  mclsrcl  30712  dfon2lem7  30938  sltval2  31053  sltres  31061  funpartlem  31219  rankeq1o  31448  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  lhpbase  34302  mapco2g  36295