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  812  ecase3d  1034  ordunidif  6361  dff3  7038  tfindsg  7801  findsg  7837  brtpos  8175  omwordi  8496  omass  8505  nnmwordi  8560  pssnn  9092  frfi  9190  ixpiunwdom  9501  cantnfp1lem3  9595  infxpenlem  9926  infxp  10127  ackbij1lem16  10147  axpowndlem3  10512  pwfseqlem4a  10574  gchina  10612  prlem936  10960  supsrlem  11024  flflp1  13729  hashunx  14311  swrdccat3blem  14663  repswswrd  14708  sumss  15649  fsumss  15650  prodss  15872  fprodss  15873  ruclem2  16159  prmind2  16614  rpexp  16651  fermltl  16713  prmreclem5  16850  ramcl  16959  wunress  17178  divsfval  17469  efgsfo  19636  lt6abl  19792  gsumval3  19804  mdetunilem8  22522  ordtrest2lem  23106  ptpjpre1  23474  fbfinnfr  23744  filufint  23823  ptcmplem2  23956  cphsqrtcl3  25103  ovoliun  25422  voliunlem3  25469  volsup  25473  cxpsqrt  26628  amgm  26917  wilthlem2  26995  sqff1o  27108  chtublem  27138  bposlem1  27211  bposlem3  27213  ostth  27566  nosupbnd1lem1  27636  noinfbnd1lem1  27651  cutlt  27863  clwwisshclwwslemlem  29975  atdmd  32360  atmd2  32362  mdsymlem4  32368  ordtrest2NEWlem  33888  eulerpartlemb  34335  dvelimalcased  35041  dvelimexcased  35043  fineqvac  35071  dfon2lem9  35764  nn0prpwlem  36295  bj-ismooredr2  37083  ltflcei  37587  poimirlem30  37629  lplnexllnN  39543  2llnjaN  39545  paddasslem14  39812  cdleme32le  40426  dgrsub2  43108  naddgeoa  43367  evenwodadd  46870  iccelpart  47418  lighneallem3  47592  lighneal  47596