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  4259  fisupg  7105  cantnff  7375  fseqenlem2  7652  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2  8265  rlimsqzlem  12122  ramub1lem2  13074  mriss  13537  invfun  13666  pltle  14095  subgslw  14927  frgpnabllem2  15162  cyggeninv  15170  ablfaclem3  15322  psrbagf  16113  mplind  16243  pjff  16612  pjf2  16614  pjfo  16615  pjcss  16616  tg1  16702  cldss  16766  cnf2  16979  cncnp  17009  lly1stc  17222  qtoptop2  17390  qtoprest  17408  elfm3  17645  flfelbas  17689  blgt0  17956  xblss2  17958  tngngp  18170  cfilfil  18693  iscau2  18703  caufpm  18708  cmetcaulem  18714  dvcnp2  19269  dvfsumrlim  19378  dvfsumrlim2  19379  fta1g  19553  dvdsflsumcom  20428  fsumvma  20452  vmadivsumb  20632  dchrisumlema  20637  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasumiflem1  20650  selbergb  20698  selberg2b  20701  pntibndlem3  20741  pntlem3  20758  sspnv  21302  lnof  21333  bloln  21362  cvmliftmolem1  23812  cvmlift2lem9a  23834  fmamo  25836  refbas  26280  ismtyres  26532  ghomf  26572  rngoisohom  26611  pridlidl  26660  pridlnr  26661  maxidlidl  26666  pell1234qrre  26937  lnmlsslnm  27179  stoweidlem34  27783  lflf  29253  lkrcl  29282  cvrlt  29460  cvrle  29468  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  psubssat  29943  lhpbase  30187  laut1o  30274  ldillaut  30300  ltrnldil  30311  diadmclN  31227
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