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  813  ecase3d  1035  ordunidif  6375  dff3  7054  tfindsg  7813  findsg  7849  brtpos  8187  omwordi  8508  omass  8517  nnmwordi  8573  pssnn  9105  frfi  9197  ixpiunwdom  9507  cantnfp1lem3  9601  infxpenlem  9935  infxp  10136  ackbij1lem16  10156  axpowndlem3  10522  pwfseqlem4a  10584  gchina  10622  prlem936  10970  supsrlem  11034  flflp1  13739  hashunx  14321  swrdccat3blem  14674  repswswrd  14719  sumss  15659  fsumss  15660  prodss  15882  fprodss  15883  ruclem2  16169  prmind2  16624  rpexp  16661  fermltl  16723  prmreclem5  16860  ramcl  16969  wunress  17188  divsfval  17480  efgsfo  19680  lt6abl  19836  gsumval3  19848  mdetunilem8  22575  ordtrest2lem  23159  ptpjpre1  23527  fbfinnfr  23797  filufint  23876  ptcmplem2  24009  cphsqrtcl3  25155  ovoliun  25474  voliunlem3  25521  volsup  25525  cxpsqrt  26680  amgm  26969  wilthlem2  27047  sqff1o  27160  chtublem  27190  bposlem1  27263  bposlem3  27265  ostth  27618  nosupbnd1lem1  27688  noinfbnd1lem1  27703  cutlt  27940  clwwisshclwwslemlem  30100  atdmd  32485  atmd2  32487  mdsymlem4  32493  ordtrest2NEWlem  34099  eulerpartlemb  34545  dvelimalcased  35250  dvelimexcased  35252  fineqvac  35291  fineqvnttrclselem1  35296  dfon2lem9  36002  nn0prpwlem  36535  bj-ismooredr2  37357  ltflcei  37853  poimirlem30  37895  lplnexllnN  39934  2llnjaN  39936  paddasslem14  40203  cdleme32le  40817  dgrsub2  43486  naddgeoa  43745  evenwodadd  47239  iccelpart  47787  lighneallem3  47961  lighneal  47965