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

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
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 484 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 463 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  8106  cantnflem3OLD  8128  mapfienOLD  8134  fseqenlem2  8402  axdc3lem2  8827  fpwwe2lem12  9015  rlimsqzlem  13427  ramub1lem2  14397  invfun  15012  pltne  15442  cntzi  16159  odmulg  16371  subgslw  16429  frgpnabllem1  16665  cyggeninv  16674  ablfaclem3  16925  lsslmod  17386  evlslem3  17951  psgnevpm  18389  pjff  18507  pjf2  18509  pjcss  18511  ocvpj  18512  scmatscmid  18772  fvmptnn04ifc  19117  fvmptnn04ifd  19118  tgcl  19234  cldopn  19295  cncnp  19544  1stcelcls  19725  lly1stc  19760  qtoptop2  19932  qtopid  19938  trfg  20124  flfneii  20225  fclsbas  20254  isfcf  20267  restutop  20472  restutopopn  20473  cfiluexsm  20525  cfilufg  20528  blgt0  20634  xblss2ps  20636  xblss2  20637  mopni  20727  metrest  20759  metustblOLD  20815  metustbl  20816  restmetu  20822  cfilss  21441  caun0  21452  cmetcaulem  21459  cfilresi  21466  cmetcuspOLD  21525  cnlimci  22025  dvcl  22035  dvcnp  22054  dvcnp2  22055  dvnadd  22064  dvfsumrlimge0  22163  dvfsumrlim  22164  dvfsumrlim2  22165  fta1g  22300  plyeq0lem  22339  vieta1lem1  22437  vieta1lem2  22438  fsumharmonic  23066  dvdsflf1o  23188  dvdsflsumcom  23189  fsumvma  23213  vmadivsumb  23393  dchrisum0lem1a  23396  dchrisumlema  23398  dchrisumlem3  23401  dchrmusum2  23404  dchrvmasumlem2  23408  dchrvmasumiflem1  23411  dchrisum0fno1  23421  dchrisum0lem1b  23425  mulog2sumlem2  23445  vmalogdivsum2  23448  2vmadivsumlem  23450  selberglem2  23456  selbergb  23459  selberg2b  23462  selberg3lem1  23467  selberg4lem1  23470  pntpbnd1  23496  pntibndlem3  23502  pntlem3  23519  sspba  25313  sspg  25314  ssps  25316  sspn  25322  nmblore  25374  phpar  25412  ocorth  25882  elnlfn2  26521  fpwrelmap  27225  kerunit  27473  cnre2csqlem  27525  fmcncfil  27546  elzrhunit  27593  qqhval2lem  27595  baselsiga  27752  signsply0  28145  cvmliftmolem1  28363  mbfresfi  29636  itg2addnclem  29641  itg2addnclem2  29642  refssex  29751  fnetr  29756  sstotbnd2  29871  rngoiso1o  29983  pridl  30035  icccncfext  31226  lfli  33858  lkrf0  33890  cvrne  34078  atcvr0  34085  psubspi  34543  psubcli2N  34735  lhp1cvr  34795  lautle  34880  diadmleN  35835
  Copyright terms: Public domain W3C validator