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

Theorem simprbda 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
simprbda  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem simprbda
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 472 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 447 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  elrabi  3092  oteqex  4451  fisupg  7357  cantnff  7631  fseqenlem2  7908  fpwwe2lem11  8517  fpwwe2lem12  8518  fpwwe2  8520  rlimsqzlem  12444  ramub1lem2  13397  mriss  13862  invfun  13991  pltle  14420  subgslw  15252  frgpnabllem2  15487  cyggeninv  15495  ablfaclem3  15647  psrbagf  16434  mplind  16564  pjff  16941  pjf2  16943  pjfo  16944  pjcss  16945  tg1  17031  cldss  17095  cnf2  17315  cncnp  17346  lly1stc  17561  qtoptop2  17733  qtoprest  17751  elfm3  17984  flfelbas  18028  cnextf  18099  restutopopn  18270  cfilufbas  18321  fmucnd  18324  blgt0  18431  xblss2ps  18433  xblss2  18434  tngngp  18697  cfilfil  19222  iscau2  19232  caufpm  19237  cmetcaulem  19243  dvcnp2  19808  dvfsumrlim  19917  dvfsumrlim2  19918  fta1g  20092  dvdsflsumcom  20975  fsumvma  20999  vmadivsumb  21179  dchrisumlema  21184  dchrvmasumlem1  21191  dchrvmasum2lem  21192  dchrvmasumiflem1  21197  selbergb  21245  selberg2b  21248  pntibndlem3  21288  pntlem3  21305  sspnv  22227  lnof  22258  bloln  22287  cvmliftmolem1  24970  cvmlift2lem9a  24992  mbfresfi  26255  itg2gt0cn  26262  refbas  26362  ismtyres  26519  ghomf  26559  rngoisohom  26598  pridlidl  26647  pridlnr  26648  maxidlidl  26653  pell1234qrre  26917  lnmlsslnm  27158  stoweidlem34  27761  lflf  29923  lkrcl  29952  cvrlt  30130  cvrle  30138  atbase  30149  llnbase  30368  lplnbase  30393  lvolbase  30437  psubssat  30613  lhpbase  30857  laut1o  30944  ldillaut  30970  ltrnldil  30981  diadmclN  31897
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 179  df-an 362
  Copyright terms: Public domain W3C validator