Theorem pm2.61d 179

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61d.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
pm2.61d	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2	1	con1d 145	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 47	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 127	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:  pm2.61d1  180  pm2.61d2  181  pm5.21ndd  379  bija  380  pm2.61dan  813  ecase3d  1035  ordunidif  6365  dff3  7044  tfindsg  7803  findsg  7839  brtpos  8176  omwordi  8497  omass  8506  nnmwordi  8562  pssnn  9094  frfi  9186  ixpiunwdom  9496  cantnfp1lem3  9590  infxpenlem  9924  infxp  10125  ackbij1lem16  10145  axpowndlem3  10511  pwfseqlem4a  10573  gchina  10611  prlem936  10959  supsrlem  11023  flflp1  13755  hashunx  14337  swrdccat3blem  14690  repswswrd  14735  sumss  15675  fsumss  15676  prodss  15901  fprodss  15902  ruclem2  16188  prmind2  16643  rpexp  16681  fermltl  16743  prmreclem5  16880  ramcl  16989  wunress  17208  divsfval  17500  efgsfo  19703  lt6abl  19859  gsumval3  19871  mdetunilem8  22593  ordtrest2lem  23177  ptpjpre1  23545  fbfinnfr  23815  filufint  23894  ptcmplem2  24027  cphsqrtcl3  25163  ovoliun  25481  voliunlem3  25528  volsup  25532  cxpsqrt  26683  amgm  26972  wilthlem2  27050  sqff1o  27163  chtublem  27193  bposlem1  27266  bposlem3  27268  ostth  27621  nosupbnd1lem1  27691  noinfbnd1lem1  27706  cutlt  27943  clwwisshclwwslemlem  30103  atdmd  32489  atmd2  32491  mdsymlem4  32497  ordtrest2NEWlem  34087  eulerpartlemb  34533  dvelimalcased  35238  dvelimexcased  35240  fineqvac  35281  fineqvnttrclselem1  35286  dfon2lem9  35992  nn0prpwlem  36525  axtcond  36681  bj-ismooredr2  37435  ltflcei  37940  poimirlem30  37982  lplnexllnN  40021  2llnjaN  40023  paddasslem14  40290  cdleme32le  40904  dgrsub2  43578  naddgeoa  43837  evenwodadd  47330  iccelpart  47890  lighneallem3  48067  lighneal  48071