Theorem pm2.61d 181

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 146	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 48	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 128	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61d1  182  pm2.61d2  183  pm5.21ndd  382  bija  383  pm2.61dan  825  ecase3d  1050  ordunidif  6412  dff3  7097  tfindsg  7861  findsg  7898  brtpos  8237  omwordi  8562  omass  8571  nnmwordi  8627  pssnn  9167  frfi  9259  ixpiunwdom  9566  cantnfp1lem3  9663  infxpenlem  10020  infxp  10220  ackbij1lem16  10240  axpowndlem3  10612  pwfseqlem4a  10674  gchina  10712  prlem936  11060  supsrlem  11124  flflp1  13872  hashunx  14454  swrdccat3blem  14812  repswswrd  14859  sumss  15814  fsumss  15815  prodss  16040  fprodss  16041  ruclem2  16326  prmind2  16781  rpexp  16819  fermltl  16881  prmreclem5  17018  ramcl  17127  wunress  17347  divsfval  17639  efgsfo  19872  lt6abl  20028  gsumval3  20040  mdetunilem8  22847  ordtrest2lem  23434  ptpjpre1  23803  fbfinnfr  24073  filufint  24152  ptcmplem2  24285  cphsqrtcl3  25421  ovoliun  25739  voliunlem3  25786  volsup  25790  cxpsqrt  26948  amgm  27235  wilthlem2  27313  sqff1o  27426  chtublem  27455  bposlem1  27528  bposlem3  27530  ostth  27883  nosupbnd1lem1  27952  noinfbnd1lem1  27967  cutlt  28205  clwwisshclwwslemlem  30491  atdmd  32887  atmd2  32889  mdsymlem4  32895  ordtrest2NEWlem  34440  eulerpartlemb  34887  dvelimalcased  35592  dvelimexcased  35594  fineqvac  35650  fineqvnttrclselem1  35655  dfon2lem9  36376  nn0prpwlem  36949  axtcond  37105  bj-ismooredr2  37868  ltflcei  38370  poimirlem30  38407  lplnexllnN  40445  2llnjaN  40447  paddasslem14  40714  cdleme32le  41328  dgrsub2  43984  naddgeoa  44243  evenwodadd  47737  iccelpart  48341  lighneallem3  48518  lighneal  48522  prmringnzring  49260