Theorem simplbda 628

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  cantnflem3  8204  fseqenlem2  8463  axdc3lem2  8888  fpwwe2lem12  9073  rlimsqzlem  13711  ramub1lem2  14984  invfun  15668  pltne  16207  cntzi  16982  odmulg  17206  subgslw  17267  frgpnabllem1  17508  cyggeninv  17517  ablfaclem3  17719  lsslmod  18182  evlslem3  18736  psgnevpm  19155  pjff  19273  pjf2  19275  pjcss  19277  ocvpj  19278  scmatscmid  19529  fvmptnn04ifc  19874  fvmptnn04ifd  19875  tgcl  19983  cldopn  20044  cncnp  20294  1stcelcls  20474  lly1stc  20509  refssex  20524  qtoptop2  20712  qtopid  20718  trfg  20904  flfneii  21005  fclsbas  21034  isfcf  21047  restutop  21250  restutopopn  21251  isucn2  21292  cfiluexsm  21303  cfilufg  21306  blgt0  21412  xblss2ps  21414  xblss2  21415  mopni  21505  metrest  21537  metustbl  21579  restmetu  21583  cfilss  22238  caun0  22249  cmetcaulem  22256  cfilresi  22263  cmetcusp  22319  cnlimci  22842  dvcl  22852  dvcnp  22871  dvcnp2  22872  dvnadd  22881  dvfsumrlimge0  22980  dvfsumrlim  22981  dvfsumrlim2  22982  fta1g  23116  plyeq0lem  23162  vieta1lem1  23261  vieta1lem2  23262  fsumharmonic  23935  dvdsflf1o  24114  dvdsflsumcom  24115  fsumvma  24139  vmadivsumb  24319  dchrisum0lem1a  24322  dchrisumlema  24324  dchrisumlem3  24327  dchrmusum2  24330  dchrvmasumlem2  24334  dchrvmasumiflem1  24337  dchrisum0fno1  24347  dchrisum0lem1b  24351  mulog2sumlem2  24371  vmalogdivsum2  24374  2vmadivsumlem  24376  selberglem2  24382  selbergb  24385  selberg2b  24388  selberg3lem1  24393  selberg4lem1  24396  pntpbnd1  24422  pntibndlem3  24428  pntlem3  24445  oppnid  24786  sspba  26364  sspg  26365  ssps  26367  sspn  26373  nmblore  26425  phpar  26463  ocorth  26942  elnlfn2  27580  foresf1o  28138  fpwrelmap  28324  kerunit  28594  reff  28674  cnre2csqlem  28724  fmcncfil  28745  elzrhunit  28791  qqhval2lem  28793  baselsiga  28945  signsply0  29448  cvmliftmolem1  30012  mclsppslem  30229  mclspps  30230  fnetr  31012  relowlssretop  31730  mbfresfi  31951  itg2addnclem  31957  itg2addnclem2  31958  sstotbnd2  32070  rngoiso1o  32182  pridl  32234  lfli  32596  lkrf0  32628  cvrne  32816  atcvr0  32823  psubspi  33281  psubcli2N  33473  lhp1cvr  33533  lautle  33618  diadmleN  34575  cvgdvgrat  36632  radcnvrat  36633  islptre  37639  islpcn  37659  icccncfext  37705  fdivmptf  39973  refdivmptf  39974  rege1logbrege0  39990