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  3263  oteqex  4746  fisupg  7780  cantnff  8105  fseqenlem2  8418  fpwwe2lem11  9030  fpwwe2lem12  9031  fpwwe2  9033  rlimsqzlem  13451  ramub1lem2  14421  mriss  14907  invfun  15036  pltle  15465  subgslw  16509  frgpnabllem2  16751  cyggeninv  16759  ablfaclem3  17010  psrbagf  17884  mplind  18037  pjff  18612  pjf2  18614  pjfo  18615  pjcss  18616  fvmptnn04ifc  19222  chfacfisf  19224  chfacfisfcpmat  19225  tg1  19334  cldss  19398  cnf2  19618  cncnp  19649  lly1stc  19865  refbas  19879  qtoptop2  20068  qtoprest  20086  elfm3  20319  flfelbas  20363  cnextf  20434  restutopopn  20609  cfilufbas  20660  fmucnd  20663  blgt0  20770  xblss2ps  20772  xblss2  20773  tngngp  21036  cfilfil  21574  iscau2  21584  caufpm  21589  cmetcaulem  21595  dvcnp2  22191  dvfsumrlim  22300  dvfsumrlim2  22301  fta1g  22436  dvdsflsumcom  23330  fsumvma  23354  vmadivsumb  23534  dchrisumlema  23539  dchrvmasumlem1  23546  dchrvmasum2lem  23547  dchrvmasumiflem1  23552  selbergb  23600  selberg2b  23603  pntibndlem3  23643  pntlem3  23660  motgrp  23796  clwlkiswlk  24571  sspnv  25453  lnof  25484  bloln  25513  reff  27658  signsply0  28324  cvmliftmolem1  28542  cvmlift2lem9a  28564  mbfresfi  29979  itg2gt0cn  29988  ismtyres  30222  ghomf  30262  rngoisohom  30301  pridlidl  30350  pridlnr  30351  maxidlidl  30356  pell1234qrre  30707  lnmlsslnm  30946  stoweidlem34  31648  lflf  34216  lkrcl  34245  cvrlt  34423  cvrle  34431  atbase  34442  llnbase  34661  lplnbase  34686  lvolbase  34730  psubssat  34906  lhpbase  35150  laut1o  35237  ldillaut  35263  ltrnldil  35274  diadmclN  36190
  Copyright terms: Public domain W3C validator