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  6367  dff3  7046  tfindsg  7805  findsg  7841  brtpos  8178  omwordi  8499  omass  8508  nnmwordi  8564  pssnn  9096  frfi  9188  ixpiunwdom  9498  cantnfp1lem3  9592  infxpenlem  9926  infxp  10127  ackbij1lem16  10147  axpowndlem3  10513  pwfseqlem4a  10575  gchina  10613  prlem936  10961  supsrlem  11025  flflp1  13757  hashunx  14339  swrdccat3blem  14692  repswswrd  14737  sumss  15677  fsumss  15678  prodss  15903  fprodss  15904  ruclem2  16190  prmind2  16645  rpexp  16683  fermltl  16745  prmreclem5  16882  ramcl  16991  wunress  17210  divsfval  17502  efgsfo  19705  lt6abl  19861  gsumval3  19873  mdetunilem8  22594  ordtrest2lem  23178  ptpjpre1  23546  fbfinnfr  23816  filufint  23895  ptcmplem2  24028  cphsqrtcl3  25164  ovoliun  25482  voliunlem3  25529  volsup  25533  cxpsqrt  26680  amgm  26968  wilthlem2  27046  sqff1o  27159  chtublem  27188  bposlem1  27261  bposlem3  27263  ostth  27616  nosupbnd1lem1  27686  noinfbnd1lem1  27701  cutlt  27938  clwwisshclwwslemlem  30098  atdmd  32484  atmd2  32486  mdsymlem4  32492  ordtrest2NEWlem  34082  eulerpartlemb  34528  dvelimalcased  35233  dvelimexcased  35235  fineqvac  35276  fineqvnttrclselem1  35281  dfon2lem9  35987  nn0prpwlem  36520  axtcond  36676  bj-ismooredr2  37438  ltflcei  37943  poimirlem30  37985  lplnexllnN  40024  2llnjaN  40026  paddasslem14  40293  cdleme32le  40907  dgrsub2  43581  naddgeoa  43840  evenwodadd  47333  iccelpart  47905  lighneallem3  48082  lighneal  48086