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  6444  dff3  7134  tfindsg  7898  findsg  7937  brtpos  8276  omwordi  8627  omass  8636  nnmwordi  8691  pssnn  9234  frfi  9349  ixpiunwdom  9659  cantnfp1lem3  9749  infxpenlem  10082  infxp  10283  ackbij1lem16  10303  axpowndlem3  10668  pwfseqlem4a  10730  gchina  10768  prlem936  11116  supsrlem  11180  flflp1  13858  hashunx  14435  swrdccat3blem  14787  repswswrd  14832  sumss  15772  fsumss  15773  prodss  15995  fprodss  15996  ruclem2  16280  prmind2  16732  rpexp  16769  fermltl  16831  prmreclem5  16967  ramcl  17076  wunress  17309  wunressOLD  17310  divsfval  17607  efgsfo  19781  lt6abl  19937  gsumval3  19949  mdetunilem8  22646  ordtrest2lem  23232  ptpjpre1  23600  fbfinnfr  23870  filufint  23949  ptcmplem2  24082  cphsqrtcl3  25240  ovoliun  25559  voliunlem3  25606  volsup  25610  cxpsqrt  26763  amgm  27052  wilthlem2  27130  sqff1o  27243  chtublem  27273  bposlem1  27346  bposlem3  27348  ostth  27701  nosupbnd1lem1  27771  noinfbnd1lem1  27786  cutlt  27984  clwwisshclwwslemlem  30045  atdmd  32430  atmd2  32432  mdsymlem4  32438  ordtrest2NEWlem  33868  eulerpartlemb  34333  dvelimalcased  35051  dvelimexcased  35053  fineqvac  35073  dfon2lem9  35755  nn0prpwlem  36288  bj-ismooredr2  37076  ltflcei  37568  poimirlem30  37610  lplnexllnN  39521  2llnjaN  39523  paddasslem14  39790  cdleme32le  40404  dgrsub2  43092  naddgeoa  43356  iccelpart  47307  lighneallem3  47481  lighneal  47485