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

Theorem simplbda 608
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 471 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 450 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  cantnflem3  7580  mapfien  7586  fseqenlem2  7839  axdc3lem2  8264  fpwwe2lem12  8449  rlimsqzlem  12369  ramub1lem2  13322  invfun  13916  pltne  14346  cntzi  15055  odmulg  15119  subgslw  15177  frgpnabllem1  15411  cyggeninv  15420  ablfaclem3  15572  lsslmod  15963  pjff  16862  pjf2  16864  pjcss  16866  ocvpj  16867  tgcl  16957  cldopn  17018  cncnp  17266  1stcelcls  17445  lly1stc  17480  qtoptop2  17652  qtopid  17658  trfg  17844  flfneii  17945  fclsbas  17974  isfcf  17987  restutop  18188  restutopopn  18189  cfiluexsm  18241  cfilufg  18244  blgt0  18330  xblss2  18332  mopni  18412  metrest  18444  metustbl  18486  restmetu  18489  cfilss  19094  caun0  19105  cmetcaulem  19112  cfilresi  19119  cmetcusp  19175  cnlimci  19643  dvcl  19653  dvcnp  19672  dvcnp2  19673  dvnadd  19682  dvfsumrlimge0  19781  dvfsumrlim  19782  dvfsumrlim2  19783  evlslem3  19802  fta1g  19957  plyeq0lem  19996  vieta1lem1  20094  vieta1lem2  20095  fsumharmonic  20717  dvdsflf1o  20839  dvdsflsumcom  20840  fsumvma  20864  vmadivsumb  21044  dchrisum0lem1a  21047  dchrisumlema  21049  dchrisumlem3  21052  dchrmusum2  21055  dchrvmasumlem2  21059  dchrvmasumiflem1  21062  dchrisum0fno1  21072  dchrisum0lem1b  21076  mulog2sumlem2  21096  vmalogdivsum2  21099  2vmadivsumlem  21101  selberglem2  21107  selbergb  21110  selberg2b  21113  selberg3lem1  21118  selberg4lem1  21121  pntpbnd1  21147  pntibndlem3  21153  pntlem3  21170  sspba  22074  sspg  22075  ssps  22077  sspn  22083  nmblore  22135  phpar  22173  ocorth  22641  elnlfn2  23280  kerunit  24077  cnre2csqlem  24112  fmcncfil  24121  elzrhunit  24162  qqhval2lem  24164  baselsiga  24294  cvmliftmolem1  24747  itg2addnclem  25957  itg2addnclem2  25958  refssex  26052  fnetr  26057  sstotbnd2  26174  rngoiso1o  26286  pridl  26338  lfli  29176  lkrf0  29208  cvrne  29396  atcvr0  29403  psubspi  29861  psubcli2N  30053  lhp1cvr  30113  lautle  30198  diadmleN  31153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator