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  6373  dff3  7052  tfindsg  7812  findsg  7848  brtpos  8185  omwordi  8506  omass  8515  nnmwordi  8571  pssnn  9103  frfi  9195  ixpiunwdom  9505  cantnfp1lem3  9601  infxpenlem  9935  infxp  10136  ackbij1lem16  10156  axpowndlem3  10522  pwfseqlem4a  10584  gchina  10622  prlem936  10970  supsrlem  11034  flflp1  13766  hashunx  14348  swrdccat3blem  14701  repswswrd  14746  sumss  15686  fsumss  15687  prodss  15912  fprodss  15913  ruclem2  16199  prmind2  16654  rpexp  16692  fermltl  16754  prmreclem5  16891  ramcl  17000  wunress  17219  divsfval  17511  efgsfo  19714  lt6abl  19870  gsumval3  19882  mdetunilem8  22584  ordtrest2lem  23168  ptpjpre1  23536  fbfinnfr  23806  filufint  23885  ptcmplem2  24018  cphsqrtcl3  25154  ovoliun  25472  voliunlem3  25519  volsup  25523  cxpsqrt  26667  amgm  26954  wilthlem2  27032  sqff1o  27145  chtublem  27174  bposlem1  27247  bposlem3  27249  ostth  27602  nosupbnd1lem1  27672  noinfbnd1lem1  27687  cutlt  27924  clwwisshclwwslemlem  30083  atdmd  32469  atmd2  32471  mdsymlem4  32477  ordtrest2NEWlem  34066  eulerpartlemb  34512  dvelimalcased  35217  dvelimexcased  35219  fineqvac  35260  fineqvnttrclselem1  35265  dfon2lem9  35971  nn0prpwlem  36504  axtcond  36660  bj-ismooredr2  37422  ltflcei  37929  poimirlem30  37971  lplnexllnN  40010  2llnjaN  40012  paddasslem14  40279  cdleme32le  40893  dgrsub2  43563  naddgeoa  43822  evenwodadd  47317  iccelpart  47893  lighneallem3  48070  lighneal  48074