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  6382  dff3  7072  tfindsg  7837  findsg  7873  brtpos  8214  omwordi  8535  omass  8544  nnmwordi  8599  pssnn  9132  frfi  9232  ixpiunwdom  9543  cantnfp1lem3  9633  infxpenlem  9966  infxp  10167  ackbij1lem16  10187  axpowndlem3  10552  pwfseqlem4a  10614  gchina  10652  prlem936  11000  supsrlem  11064  flflp1  13769  hashunx  14351  swrdccat3blem  14704  repswswrd  14749  sumss  15690  fsumss  15691  prodss  15913  fprodss  15914  ruclem2  16200  prmind2  16655  rpexp  16692  fermltl  16754  prmreclem5  16891  ramcl  17000  wunress  17219  divsfval  17510  efgsfo  19669  lt6abl  19825  gsumval3  19837  mdetunilem8  22506  ordtrest2lem  23090  ptpjpre1  23458  fbfinnfr  23728  filufint  23807  ptcmplem2  23940  cphsqrtcl3  25087  ovoliun  25406  voliunlem3  25453  volsup  25457  cxpsqrt  26612  amgm  26901  wilthlem2  26979  sqff1o  27092  chtublem  27122  bposlem1  27195  bposlem3  27197  ostth  27550  nosupbnd1lem1  27620  noinfbnd1lem1  27635  cutlt  27840  clwwisshclwwslemlem  29942  atdmd  32327  atmd2  32329  mdsymlem4  32335  ordtrest2NEWlem  33912  eulerpartlemb  34359  dvelimalcased  35065  dvelimexcased  35067  fineqvac  35087  dfon2lem9  35779  nn0prpwlem  36310  bj-ismooredr2  37098  ltflcei  37602  poimirlem30  37644  lplnexllnN  39558  2llnjaN  39560  paddasslem14  39827  cdleme32le  40441  dgrsub2  43124  naddgeoa  43383  evenwodadd  46886  iccelpart  47434  lighneallem3  47608  lighneal  47612