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

Theorem simprbda 606
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 470 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 445 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  oteqex  4275  fisupg  7121  cantnff  7391  fseqenlem2  7668  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2  8281  rlimsqzlem  12138  ramub1lem2  13090  mriss  13553  invfun  13682  pltle  14111  subgslw  14943  frgpnabllem2  15178  cyggeninv  15186  ablfaclem3  15338  psrbagf  16129  mplind  16259  pjff  16628  pjf2  16630  pjfo  16631  pjcss  16632  tg1  16718  cldss  16782  cnf2  16995  cncnp  17025  lly1stc  17238  qtoptop2  17406  qtoprest  17424  elfm3  17661  flfelbas  17705  blgt0  17972  xblss2  17974  tngngp  18186  cfilfil  18709  iscau2  18719  caufpm  18724  cmetcaulem  18730  dvcnp2  19285  dvfsumrlim  19394  dvfsumrlim2  19395  fta1g  19569  dvdsflsumcom  20444  fsumvma  20468  vmadivsumb  20648  dchrisumlema  20653  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasumiflem1  20666  selbergb  20714  selberg2b  20717  pntibndlem3  20757  pntlem3  20774  sspnv  21318  lnof  21349  bloln  21378  cvmliftmolem1  23827  cvmlift2lem9a  23849  itg2gt0cn  25006  fmamo  25939  refbas  26383  ismtyres  26635  ghomf  26675  rngoisohom  26714  pridlidl  26763  pridlnr  26764  maxidlidl  26769  pell1234qrre  27040  lnmlsslnm  27282  stoweidlem34  27886  lflf  29875  lkrcl  29904  cvrlt  30082  cvrle  30090  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  psubssat  30565  lhpbase  30809  laut1o  30896  ldillaut  30922  ltrnldil  30933  diadmclN  31849
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