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

Theorem simplbda 607
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 470 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 449 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  cantnflem3  7409  mapfien  7415  fseqenlem2  7668  axdc3lem2  8093  fpwwe2lem12  8279  rlimsqzlem  12138  ramub1lem2  13090  invfun  13682  pltne  14112  cntzi  14821  odmulg  14885  subgslw  14943  frgpnabllem1  15177  cyggeninv  15186  ablfaclem3  15338  lsslmod  15733  pjff  16628  pjf2  16630  pjcss  16632  ocvpj  16633  tgcl  16723  cldopn  16784  cncnp  17025  1stcelcls  17203  lly1stc  17238  qtoptop2  17406  qtopid  17412  trfg  17602  flfneii  17703  fclsbas  17732  isfcf  17745  blgt0  17972  xblss2  17974  mopni  18054  metrest  18086  cfilss  18712  caun0  18723  cmetcaulem  18730  cfilresi  18737  cnlimci  19255  dvcl  19265  dvcnp  19284  dvcnp2  19285  dvnadd  19294  dvfsumrlimge0  19393  dvfsumrlim  19394  dvfsumrlim2  19395  evlslem3  19414  fta1g  19569  plyeq0lem  19608  vieta1lem1  19706  vieta1lem2  19707  fsumharmonic  20321  dvdsflf1o  20443  dvdsflsumcom  20444  fsumvma  20468  vmadivsumb  20648  dchrisum0lem1a  20651  dchrisumlema  20653  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0fno1  20676  dchrisum0lem1b  20680  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  selberglem2  20711  selbergb  20714  selberg2b  20717  selberg3lem1  20722  selberg4lem1  20725  pntpbnd1  20751  pntibndlem3  20757  pntlem3  20774  sspba  21319  sspg  21320  ssps  21322  sspn  21328  nmblore  21380  phpar  21418  ocorth  21886  elnlfn2  22525  cvmliftmolem1  23827  itg2addnclem  25003  itg2addnclem2  25004  vidfunid  25940  iddvvidd  25941  idcvvidc  25942  fmp  25943  refssex  26384  fnetr  26389  sstotbnd2  26601  rngoiso1o  26713  pridl  26765  lfli  29873  lkrf0  29905  cvrne  30093  atcvr0  30100  psubspi  30558  psubcli2N  30750  lhp1cvr  30810  lautle  30895  diadmleN  31850
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 177  df-an 360
  Copyright terms: Public domain W3C validator