Theorem simplbda 634

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
pm3.26bda.1	|- ( ph -> ( ps <-> ( ch /\ th ) ) )

Assertion

Ref	Expression
simplbda	|- ( ( ph /\ ps ) -> th )

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
2	1	biimpa 491	. 2 |- ( ( ph /\ ps ) -> ( ch /\ th ) )
3	2	simprd 469	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190  df-an 377

This theorem is referenced by:  cantnflem3  8183  fseqenlem2  8443  axdc3lem2  8868  fpwwe2lem12  9053  rlimsqzlem  13723  ramub1lem2  14996  invfun  15680  pltne  16219  cntzi  16994  odmulg  17218  subgslw  17279  frgpnabllem1  17520  cyggeninv  17529  ablfaclem3  17731  lsslmod  18194  evlslem3  18748  psgnevpm  19168  pjff  19286  pjf2  19288  pjcss  19290  ocvpj  19291  scmatscmid  19542  fvmptnn04ifc  19887  fvmptnn04ifd  19888  tgcl  19996  cldopn  20057  cncnp  20307  1stcelcls  20487  lly1stc  20522  refssex  20537  qtoptop2  20725  qtopid  20731  trfg  20917  flfneii  21018  fclsbas  21047  isfcf  21060  restutop  21263  restutopopn  21264  isucn2  21305  cfiluexsm  21316  cfilufg  21319  blgt0  21425  xblss2ps  21427  xblss2  21428  mopni  21518  metrest  21550  metustbl  21592  restmetu  21596  cfilss  22251  caun0  22262  cmetcaulem  22269  cfilresi  22276  cmetcusp  22332  cnlimci  22856  dvcl  22866  dvcnp  22885  dvcnp2  22886  dvnadd  22895  dvfsumrlimge0  22994  dvfsumrlim  22995  dvfsumrlim2  22996  fta1g  23130  plyeq0lem  23176  vieta1lem1  23275  vieta1lem2  23276  fsumharmonic  23949  dvdsflf1o  24128  dvdsflsumcom  24129  fsumvma  24153  vmadivsumb  24333  dchrisum0lem1a  24336  dchrisumlema  24338  dchrisumlem3  24341  dchrmusum2  24344  dchrvmasumlem2  24348  dchrvmasumiflem1  24351  dchrisum0fno1  24361  dchrisum0lem1b  24365  mulog2sumlem2  24385  vmalogdivsum2  24388  2vmadivsumlem  24390  selberglem2  24396  selbergb  24399  selberg2b  24402  selberg3lem1  24407  selberg4lem1  24410  pntpbnd1  24436  pntibndlem3  24442  pntlem3  24459  oppnid  24800  sspba  26378  sspg  26379  ssps  26381  sspn  26387  nmblore  26439  phpar  26477  ocorth  26956  elnlfn2  27594  foresf1o  28151  fpwrelmap  28326  kerunit  28593  reff  28673  cnre2csqlem  28723  fmcncfil  28744  elzrhunit  28790  qqhval2lem  28792  baselsiga  28944  signsply0  29446  cvmliftmolem1  30010  mclsppslem  30227  mclspps  30228  fnetr  31013  relowlssretop  31768  mbfresfi  31989  itg2addnclem  31995  itg2addnclem2  31996  sstotbnd2  32108  rngoiso1o  32220  pridl  32272  lfli  32629  lkrf0  32661  cvrne  32849  atcvr0  32856  psubspi  33314  psubcli2N  33506  lhp1cvr  33566  lautle  33651  diadmleN  34608  cvgdvgrat  36663  radcnvrat  36664  islptre  37741  islpcn  37761  icccncfext  37807  fdivmptf  40677  refdivmptf  40678  rege1logbrege0  40694