MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbda Structured version   Unicode version

Theorem simplbda 619
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
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 481 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 460 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
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  7887  cantnflem3OLD  7909  mapfienOLD  7915  fseqenlem2  8183  axdc3lem2  8608  fpwwe2lem12  8796  rlimsqzlem  13110  ramub1lem2  14071  invfun  14685  pltne  15115  cntzi  15827  odmulg  16037  subgslw  16095  frgpnabllem1  16331  cyggeninv  16340  ablfaclem3  16562  lsslmod  16963  psgnevpm  17861  pjff  17979  pjf2  17981  pjcss  17983  ocvpj  17984  tgcl  18416  cldopn  18477  cncnp  18726  1stcelcls  18907  lly1stc  18942  qtoptop2  19114  qtopid  19120  trfg  19306  flfneii  19407  fclsbas  19436  isfcf  19449  restutop  19654  restutopopn  19655  cfiluexsm  19707  cfilufg  19710  blgt0  19816  xblss2ps  19818  xblss2  19819  mopni  19909  metrest  19941  metustblOLD  19997  metustbl  19998  restmetu  20004  cfilss  20623  caun0  20634  cmetcaulem  20641  cfilresi  20648  cmetcuspOLD  20707  cnlimci  21206  dvcl  21216  dvcnp  21235  dvcnp2  21236  dvnadd  21245  dvfsumrlimge0  21344  dvfsumrlim  21345  dvfsumrlim2  21346  evlslem3  21366  fta1g  21524  plyeq0lem  21563  vieta1lem1  21661  vieta1lem2  21662  fsumharmonic  22290  dvdsflf1o  22412  dvdsflsumcom  22413  fsumvma  22437  vmadivsumb  22617  dchrisum0lem1a  22620  dchrisumlema  22622  dchrisumlem3  22625  dchrmusum2  22628  dchrvmasumlem2  22632  dchrvmasumiflem1  22635  dchrisum0fno1  22645  dchrisum0lem1b  22649  mulog2sumlem2  22669  vmalogdivsum2  22672  2vmadivsumlem  22674  selberglem2  22680  selbergb  22683  selberg2b  22686  selberg3lem1  22691  selberg4lem1  22694  pntpbnd1  22720  pntibndlem3  22726  pntlem3  22743  sspba  23948  sspg  23949  ssps  23951  sspn  23957  nmblore  24009  phpar  24047  ocorth  24517  elnlfn2  25156  fpwrelmap  25858  kerunit  26144  cnre2csqlem  26194  fmcncfil  26215  elzrhunit  26262  qqhval2lem  26264  baselsiga  26412  signsply0  26800  cvmliftmolem1  27018  mbfresfi  28282  itg2addnclem  28287  itg2addnclem2  28288  refssex  28397  fnetr  28402  sstotbnd2  28517  rngoiso1o  28629  pridl  28681  lfli  32300  lkrf0  32332  cvrne  32520  atcvr0  32527  psubspi  32985  psubcli2N  33177  lhp1cvr  33237  lautle  33322  diadmleN  34277
  Copyright terms: Public domain W3C validator