Theorem simplbda 624

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

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

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 371

This theorem is referenced by:  cantnflem3  8009  cantnflem3OLD  8031  mapfienOLD  8037  fseqenlem2  8305  axdc3lem2  8730  fpwwe2lem12  8918  rlimsqzlem  13243  ramub1lem2  14205  invfun  14820  pltne  15250  cntzi  15965  odmulg  16177  subgslw  16235  frgpnabllem1  16471  cyggeninv  16480  ablfaclem3  16709  lsslmod  17163  evlslem3  17723  psgnevpm  18143  pjff  18261  pjf2  18263  pjcss  18265  ocvpj  18266  tgcl  18705  cldopn  18766  cncnp  19015  1stcelcls  19196  lly1stc  19231  qtoptop2  19403  qtopid  19409  trfg  19595  flfneii  19696  fclsbas  19725  isfcf  19738  restutop  19943  restutopopn  19944  cfiluexsm  19996  cfilufg  19999  blgt0  20105  xblss2ps  20107  xblss2  20108  mopni  20198  metrest  20230  metustblOLD  20286  metustbl  20287  restmetu  20293  cfilss  20912  caun0  20923  cmetcaulem  20930  cfilresi  20937  cmetcuspOLD  20996  cnlimci  21496  dvcl  21506  dvcnp  21525  dvcnp2  21526  dvnadd  21535  dvfsumrlimge0  21634  dvfsumrlim  21635  dvfsumrlim2  21636  fta1g  21771  plyeq0lem  21810  vieta1lem1  21908  vieta1lem2  21909  fsumharmonic  22537  dvdsflf1o  22659  dvdsflsumcom  22660  fsumvma  22684  vmadivsumb  22864  dchrisum0lem1a  22867  dchrisumlema  22869  dchrisumlem3  22872  dchrmusum2  22875  dchrvmasumlem2  22879  dchrvmasumiflem1  22882  dchrisum0fno1  22892  dchrisum0lem1b  22896  mulog2sumlem2  22916  vmalogdivsum2  22919  2vmadivsumlem  22921  selberglem2  22927  selbergb  22930  selberg2b  22933  selberg3lem1  22938  selberg4lem1  22941  pntpbnd1  22967  pntibndlem3  22973  pntlem3  22990  sspba  24276  sspg  24277  ssps  24279  sspn  24285  nmblore  24337  phpar  24375  ocorth  24845  elnlfn2  25484  fpwrelmap  26183  kerunit  26435  cnre2csqlem  26484  fmcncfil  26505  elzrhunit  26552  qqhval2lem  26554  baselsiga  26702  signsply0  27095  cvmliftmolem1  27313  mbfresfi  28585  itg2addnclem  28590  itg2addnclem2  28591  refssex  28700  fnetr  28705  sstotbnd2  28820  rngoiso1o  28932  pridl  28984  fvmptnn04ifc  31323  fvmptnn04ifd  31324  lfli  33029  lkrf0  33061  cvrne  33249  atcvr0  33256  psubspi  33714  psubcli2N  33906  lhp1cvr  33966  lautle  34051  diadmleN  35006