Theorem simplbda 622

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367

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 185  df-an 369

This theorem is referenced by:  cantnflem3  8041  cantnflem3OLD  8063  mapfienOLD  8069  fseqenlem2  8337  axdc3lem2  8762  fpwwe2lem12  8948  rlimsqzlem  13492  ramub1lem2  14566  invfun  15189  pltne  15728  cntzi  16503  odmulg  16714  subgslw  16772  frgpnabllem1  17013  cyggeninv  17022  ablfaclem3  17270  lsslmod  17738  evlslem3  18315  psgnevpm  18735  pjff  18853  pjf2  18855  pjcss  18857  ocvpj  18858  scmatscmid  19112  fvmptnn04ifc  19457  fvmptnn04ifd  19458  tgcl  19575  cldopn  19636  cncnp  19886  1stcelcls  20066  lly1stc  20101  refssex  20116  qtoptop2  20304  qtopid  20310  trfg  20496  flfneii  20597  fclsbas  20626  isfcf  20639  restutop  20844  restutopopn  20845  isucn2  20886  cfiluexsm  20897  cfilufg  20900  blgt0  21006  xblss2ps  21008  xblss2  21009  mopni  21099  metrest  21131  metustblOLD  21187  metustbl  21188  restmetu  21194  cfilss  21813  caun0  21824  cmetcaulem  21831  cfilresi  21838  cmetcuspOLD  21897  cmetcusp  21898  cnlimci  22397  dvcl  22407  dvcnp  22426  dvcnp2  22427  dvnadd  22436  dvfsumrlimge0  22535  dvfsumrlim  22536  dvfsumrlim2  22537  fta1g  22672  plyeq0lem  22711  vieta1lem1  22810  vieta1lem2  22811  fsumharmonic  23477  dvdsflf1o  23599  dvdsflsumcom  23600  fsumvma  23624  vmadivsumb  23804  dchrisum0lem1a  23807  dchrisumlema  23809  dchrisumlem3  23812  dchrmusum2  23815  dchrvmasumlem2  23819  dchrvmasumiflem1  23822  dchrisum0fno1  23832  dchrisum0lem1b  23836  mulog2sumlem2  23856  vmalogdivsum2  23859  2vmadivsumlem  23861  selberglem2  23867  selbergb  23870  selberg2b  23873  selberg3lem1  23878  selberg4lem1  23881  pntpbnd1  23907  pntibndlem3  23913  pntlem3  23930  oppnid  24259  sspba  25778  sspg  25779  ssps  25781  sspn  25787  nmblore  25839  phpar  25877  ocorth  26347  elnlfn2  26985  foresf1o  27544  fpwrelmap  27736  kerunit  27998  reff  28027  cnre2csqlem  28077  fmcncfil  28098  elzrhunit  28144  qqhval2lem  28146  baselsiga  28295  signsply0  28727  cvmliftmolem1  28951  mclsppslem  29168  mclspps  29169  mbfresfi  30262  itg2addnclem  30268  itg2addnclem2  30269  fnetr  30371  sstotbnd2  30472  rngoiso1o  30584  pridl  30636  cvgdvgrat  31398  radcnvrat  31399  islptre  31826  islpcn  31846  icccncfext  31891  fdivmptf  33397  refdivmptf  33398  rege1logbrege0  33414  lfli  35234  lkrf0  35266  cvrne  35454  atcvr0  35461  psubspi  35919  psubcli2N  36111  lhp1cvr  36171  lautle  36256  diadmleN  37213