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

Theorem simprbda 627
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 486 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 460 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  elrabi  3226  oteqex  4710  fsnex  6193  fisupg  7822  fiinfg  8018  cantnff  8181  fseqenlem2  8457  fpwwe2lem11  9066  fpwwe2lem12  9067  fpwwe2  9069  rlimsqzlem  13700  ramub1lem2  14973  mriss  15529  invfun  15657  pltle  16195  subgslw  17256  frgpnabllem2  17498  cyggeninv  17506  ablfaclem3  17708  psrbagf  18577  mplind  18713  pjff  19262  pjf2  19264  pjfo  19265  pjcss  19266  fvmptnn04ifc  19863  chfacfisf  19865  chfacfisfcpmat  19866  tg1  19966  cldss  20031  cnf2  20252  cncnp  20283  lly1stc  20498  refbas  20512  qtoptop2  20701  qtoprest  20719  elfm3  20952  flfelbas  20996  cnextf  21068  restutopopn  21240  cfilufbas  21291  fmucnd  21294  blgt0  21401  xblss2ps  21403  xblss2  21404  tngngp  21649  cfilfil  22224  iscau2  22234  caufpm  22239  cmetcaulem  22245  dvcnp2  22861  dvfsumrlim  22970  dvfsumrlim2  22971  fta1g  23105  dvdsflsumcom  24104  fsumvma  24128  vmadivsumb  24308  dchrisumlema  24313  dchrvmasumlem1  24320  dchrvmasum2lem  24321  dchrvmasumiflem1  24326  selbergb  24374  selberg2b  24377  pntibndlem3  24417  pntlem3  24434  motgrp  24575  oppnid  24775  clwlkiswlk  25471  sspnv  26351  lnof  26382  bloln  26411  reff  28662  signsply0  29436  cvmliftmolem1  30000  cvmlift2lem9a  30022  mbfresfi  31901  itg2gt0cn  31911  ismtyres  32054  ghomf  32094  rngoisohom  32133  pridlidl  32182  pridlnr  32183  maxidlidl  32188  lflf  32548  lkrcl  32577  cvrlt  32755  cvrle  32763  atbase  32774  llnbase  32993  lplnbase  33018  lvolbase  33062  psubssat  33238  lhpbase  33482  laut1o  33569  ldillaut  33595  ltrnldil  33606  diadmclN  34524  pell1234qrre  35618  lnmlsslnm  35859  cvgdvgrat  36520  stoweidlem34  37715
  Copyright terms: Public domain W3C validator