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

Theorem simprbda 623
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
Hypothesis
Ref Expression
pm3.26bda.1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
simprbda  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem simprbda
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 484 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 459 1  |-  ( (
ph  /\  ps )  ->  ch )
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:  elrabi  3113  oteqex  4583  fisupg  7559  cantnff  7881  fseqenlem2  8194  fpwwe2lem11  8806  fpwwe2lem12  8807  fpwwe2  8809  rlimsqzlem  13125  ramub1lem2  14087  mriss  14572  invfun  14701  pltle  15130  subgslw  16114  frgpnabllem2  16351  cyggeninv  16359  ablfaclem3  16587  psrbagf  17431  mplind  17583  pjff  18136  pjf2  18138  pjfo  18139  pjcss  18140  tg1  18568  cldss  18632  cnf2  18852  cncnp  18883  lly1stc  19099  qtoptop2  19271  qtoprest  19289  elfm3  19522  flfelbas  19566  cnextf  19637  restutopopn  19812  cfilufbas  19863  fmucnd  19866  blgt0  19973  xblss2ps  19975  xblss2  19976  tngngp  20239  cfilfil  20777  iscau2  20787  caufpm  20792  cmetcaulem  20798  dvcnp2  21393  dvfsumrlim  21502  dvfsumrlim2  21503  fta1g  21638  dvdsflsumcom  22527  fsumvma  22551  vmadivsumb  22731  dchrisumlema  22736  dchrvmasumlem1  22743  dchrvmasum2lem  22744  dchrvmasumiflem1  22749  selbergb  22797  selberg2b  22800  pntibndlem3  22840  pntlem3  22857  sspnv  24123  lnof  24154  bloln  24183  signsply0  26951  cvmliftmolem1  27169  cvmlift2lem9a  27191  mbfresfi  28436  itg2gt0cn  28445  refbas  28550  ismtyres  28705  ghomf  28745  rngoisohom  28784  pridlidl  28833  pridlnr  28834  maxidlidl  28839  pell1234qrre  29191  lnmlsslnm  29432  stoweidlem34  29827  clwlkiswlk  30420  lflf  32706  lkrcl  32735  cvrlt  32913  cvrle  32921  atbase  32932  llnbase  33151  lplnbase  33176  lvolbase  33220  psubssat  33396  lhpbase  33640  laut1o  33727  ldillaut  33753  ltrnldil  33764  diadmclN  34680
  Copyright terms: Public domain W3C validator