Theorem pm2.61d 180

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  181  pm2.61d2  182  pm5.21ndd  381  bija  382  pm2.61dan  822  ecase3d  1045  ordunidif  6392  dff3  7077  tfindsg  7837  findsg  7874  brtpos  8210  omwordi  8535  omass  8544  nnmwordi  8600  pssnn  9133  frfi  9225  ixpiunwdom  9535  cantnfp1lem3  9632  infxpenlem  9966  infxp  10167  ackbij1lem16  10187  axpowndlem3  10554  pwfseqlem4a  10616  gchina  10654  prlem936  11002  supsrlem  11066  flflp1  13814  hashunx  14396  swrdccat3blem  14749  repswswrd  14794  sumss  15734  fsumss  15735  prodss  15960  fprodss  15961  ruclem2  16247  prmind2  16702  rpexp  16740  fermltl  16802  prmreclem5  16939  ramcl  17048  wunress  17268  divsfval  17560  efgsfo  19762  lt6abl  19918  gsumval3  19930  mdetunilem8  22659  ordtrest2lem  23243  ptpjpre1  23611  fbfinnfr  23881  filufint  23960  ptcmplem2  24093  cphsqrtcl3  25229  ovoliun  25547  voliunlem3  25594  volsup  25598  cxpsqrt  26745  amgm  27032  wilthlem2  27110  sqff1o  27223  chtublem  27252  bposlem1  27325  bposlem3  27327  ostth  27680  nosupbnd1lem1  27749  noinfbnd1lem1  27764  cutlt  28002  clwwisshclwwslemlem  30161  atdmd  32547  atmd2  32549  mdsymlem4  32555  ordtrest2NEWlem  34180  eulerpartlemb  34626  dvelimalcased  35334  dvelimexcased  35336  fineqvac  35376  fineqvnttrclselem1  35381  dfon2lem9  36103  nn0prpwlem  36646  axtcond  36802  bj-ismooredr2  37564  ltflcei  38071  poimirlem30  38113  lplnexllnN  40152  2llnjaN  40154  paddasslem14  40421  cdleme32le  41035  dgrsub2  43676  naddgeoa  43935  evenwodadd  47427  iccelpart  48003  lighneallem3  48180  lighneal  48184