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  7891  cantnflem3OLD  7913  mapfienOLD  7919  fseqenlem2  8187  axdc3lem2  8612  fpwwe2lem12  8800  rlimsqzlem  13118  ramub1lem2  14080  invfun  14694  pltne  15124  cntzi  15838  odmulg  16048  subgslw  16106  frgpnabllem1  16342  cyggeninv  16351  ablfaclem3  16576  lsslmod  17018  evlslem3  17575  psgnevpm  17994  pjff  18112  pjf2  18114  pjcss  18116  ocvpj  18117  tgcl  18549  cldopn  18610  cncnp  18859  1stcelcls  19040  lly1stc  19075  qtoptop2  19247  qtopid  19253  trfg  19439  flfneii  19540  fclsbas  19569  isfcf  19582  restutop  19787  restutopopn  19788  cfiluexsm  19840  cfilufg  19843  blgt0  19949  xblss2ps  19951  xblss2  19952  mopni  20042  metrest  20074  metustblOLD  20130  metustbl  20131  restmetu  20137  cfilss  20756  caun0  20767  cmetcaulem  20774  cfilresi  20781  cmetcuspOLD  20840  cnlimci  21339  dvcl  21349  dvcnp  21368  dvcnp2  21369  dvnadd  21378  dvfsumrlimge0  21477  dvfsumrlim  21478  dvfsumrlim2  21479  fta1g  21614  plyeq0lem  21653  vieta1lem1  21751  vieta1lem2  21752  fsumharmonic  22380  dvdsflf1o  22502  dvdsflsumcom  22503  fsumvma  22527  vmadivsumb  22707  dchrisum0lem1a  22710  dchrisumlema  22712  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumiflem1  22725  dchrisum0fno1  22735  dchrisum0lem1b  22739  mulog2sumlem2  22759  vmalogdivsum2  22762  2vmadivsumlem  22764  selberglem2  22770  selbergb  22773  selberg2b  22776  selberg3lem1  22781  selberg4lem1  22784  pntpbnd1  22810  pntibndlem3  22816  pntlem3  22833  sspba  24076  sspg  24077  ssps  24079  sspn  24085  nmblore  24137  phpar  24175  ocorth  24645  elnlfn2  25284  fpwrelmap  25984  kerunit  26242  cnre2csqlem  26292  fmcncfil  26313  elzrhunit  26360  qqhval2lem  26362  baselsiga  26510  signsply0  26904  cvmliftmolem1  27122  mbfresfi  28391  itg2addnclem  28396  itg2addnclem2  28397  refssex  28506  fnetr  28511  sstotbnd2  28626  rngoiso1o  28738  pridl  28790  lfli  32546  lkrf0  32578  cvrne  32766  atcvr0  32773  psubspi  33231  psubcli2N  33423  lhp1cvr  33483  lautle  33568  diadmleN  34523