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  8113  cantnflem3OLD  8135  mapfienOLD  8141  fseqenlem2  8409  axdc3lem2  8834  fpwwe2lem12  9022  rlimsqzlem  13453  ramub1lem2  14527  invfun  15140  pltne  15571  cntzi  16346  odmulg  16557  subgslw  16615  frgpnabllem1  16856  cyggeninv  16865  ablfaclem3  17117  lsslmod  17585  evlslem3  18162  psgnevpm  18603  pjff  18721  pjf2  18723  pjcss  18725  ocvpj  18726  scmatscmid  18986  fvmptnn04ifc  19331  fvmptnn04ifd  19332  tgcl  19449  cldopn  19510  cncnp  19759  1stcelcls  19940  lly1stc  19975  refssex  19990  qtoptop2  20178  qtopid  20184  trfg  20370  flfneii  20471  fclsbas  20500  isfcf  20513  restutop  20718  restutopopn  20719  isucn2  20760  cfiluexsm  20771  cfilufg  20774  blgt0  20880  xblss2ps  20882  xblss2  20883  mopni  20973  metrest  21005  metustblOLD  21061  metustbl  21062  restmetu  21068  cfilss  21687  caun0  21698  cmetcaulem  21705  cfilresi  21712  cmetcuspOLD  21771  cmetcusp  21772  cnlimci  22271  dvcl  22281  dvcnp  22300  dvcnp2  22301  dvnadd  22310  dvfsumrlimge0  22409  dvfsumrlim  22410  dvfsumrlim2  22411  fta1g  22546  plyeq0lem  22585  vieta1lem1  22684  vieta1lem2  22685  fsumharmonic  23319  dvdsflf1o  23441  dvdsflsumcom  23442  fsumvma  23466  vmadivsumb  23646  dchrisum0lem1a  23649  dchrisumlema  23651  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumiflem1  23664  dchrisum0fno1  23674  dchrisum0lem1b  23678  mulog2sumlem2  23698  vmalogdivsum2  23701  2vmadivsumlem  23703  selberglem2  23709  selbergb  23712  selberg2b  23715  selberg3lem1  23720  selberg4lem1  23723  pntpbnd1  23749  pntibndlem3  23755  pntlem3  23772  oppnid  24096  sspba  25618  sspg  25619  ssps  25621  sspn  25627  nmblore  25679  phpar  25717  ocorth  26187  elnlfn2  26826  foresf1o  27381  fpwrelmap  27534  kerunit  27791  reff  27820  cnre2csqlem  27870  fmcncfil  27891  elzrhunit  27938  qqhval2lem  27940  baselsiga  28093  signsply0  28486  cvmliftmolem1  28704  mclsppslem  28921  mclspps  28922  mbfresfi  30037  itg2addnclem  30042  itg2addnclem2  30043  fnetr  30145  sstotbnd2  30246  rngoiso1o  30358  pridl  30410  cvgdvgrat  31170  radcnvrat  31171  islptre  31579  islpcn  31599  icccncfext  31644  lfli  34661  lkrf0  34693  cvrne  34881  atcvr0  34888  psubspi  35346  psubcli2N  35538  lhp1cvr  35598  lautle  35683  diadmleN  36640