Theorem simplbda 654

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 501	. 2 |- ( ( ph /\ ps ) -> ( ch /\ th ) )
3	2	simprd 479	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  cantnflem3  8588  fseqenlem2  8848  axdc3lem2  9273  fpwwe2lem12  9463  rlimsqzlem  14379  ramub1lem2  15731  invfun  16424  pltne  16962  cntzi  17762  odmulg  17973  subgslw  18031  frgpnabllem1  18276  cyggeninv  18285  ablfaclem3  18486  lsslmod  18960  evlslem3  19514  psgnevpm  19935  pjff  20056  pjf2  20058  pjcss  20060  ocvpj  20061  scmatscmid  20312  fvmptnn04ifc  20657  fvmptnn04ifd  20658  tgcl  20773  cldopn  20835  cncnp  21084  1stcelcls  21264  lly1stc  21299  refssex  21314  qtoptop2  21502  qtopid  21508  trfg  21695  flfneii  21796  fclsbas  21825  isfcf  21838  restutop  22041  restutopopn  22042  isucn2  22083  cfiluexsm  22094  cfilufg  22097  blgt0  22204  xblss2ps  22206  xblss2  22207  mopni  22297  metrest  22329  metustbl  22371  restmetu  22375  cfilss  23068  caun0  23079  cmetcaulem  23086  cfilresi  23093  cmetcusp  23150  cnlimci  23653  dvcl  23663  dvcnp  23682  dvcnp2  23683  dvnadd  23692  dvfsumrlimge0  23793  dvfsumrlim  23794  dvfsumrlim2  23795  fta1g  23927  plyeq0lem  23966  vieta1lem1  24065  vieta1lem2  24066  fsumharmonic  24738  dvdsflf1o  24913  dvdsflsumcom  24914  fsumvma  24938  vmadivsumb  25172  dchrisum0lem1a  25175  dchrisumlema  25177  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0fno1  25200  dchrisum0lem1b  25204  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  selberglem2  25235  selbergb  25238  selberg2b  25241  selberg3lem1  25246  selberg4lem1  25249  pntpbnd1  25275  pntibndlem3  25281  pntlem3  25298  oppnid  25638  sspba  27582  sspg  27583  ssps  27585  sspn  27591  nmblore  27641  phpar  27679  ocorth  28150  elnlfn2  28788  foresf1o  29343  fpwrelmap  29508  kerunit  29823  reff  29906  cnre2csqlem  29956  fmcncfil  29977  elzrhunit  30023  qqhval2lem  30025  baselsiga  30178  signsply0  30628  cvmliftmolem1  31263  mclsppslem  31480  mclspps  31481  fnetr  32346  relowlssretop  33211  mbfresfi  33456  itg2addnclem  33461  itg2addnclem2  33462  sstotbnd2  33573  rngoiso1o  33778  pridl  33836  lfli  34348  lkrf0  34380  cvrne  34568  atcvr0  34575  psubspi  35033  psubcli2N  35225  lhp1cvr  35285  lautle  35370  diadmleN  36327  cvgdvgrat  38512  radcnvrat  38513  islptre  39851  islpcn  39871  icccncfext  40100  fdivmptf  42335  refdivmptf  42336  rege1logbrege0  42352