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

Theorem simprbda 621
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 482 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 457 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  elrabi  3203  oteqex  4682  fsnex  6168  fisupg  7801  cantnff  8124  fseqenlem2  8437  fpwwe2lem11  9047  fpwwe2lem12  9048  fpwwe2  9050  rlimsqzlem  13618  ramub1lem2  14752  mriss  15247  invfun  15375  pltle  15913  subgslw  16958  frgpnabllem2  17200  cyggeninv  17208  ablfaclem3  17456  psrbagf  18332  mplind  18485  pjff  19039  pjf2  19041  pjfo  19042  pjcss  19043  fvmptnn04ifc  19643  chfacfisf  19645  chfacfisfcpmat  19646  tg1  19755  cldss  19820  cnf2  20041  cncnp  20072  lly1stc  20287  refbas  20301  qtoptop2  20490  qtoprest  20508  elfm3  20741  flfelbas  20785  cnextf  20856  restutopopn  21031  cfilufbas  21082  fmucnd  21085  blgt0  21192  xblss2ps  21194  xblss2  21195  tngngp  21458  cfilfil  21996  iscau2  22006  caufpm  22011  cmetcaulem  22017  dvcnp2  22613  dvfsumrlim  22722  dvfsumrlim2  22723  fta1g  22858  dvdsflsumcom  23843  fsumvma  23867  vmadivsumb  24047  dchrisumlema  24052  dchrvmasumlem1  24059  dchrvmasum2lem  24060  dchrvmasumiflem1  24065  selbergb  24113  selberg2b  24116  pntibndlem3  24156  pntlem3  24173  motgrp  24311  oppnid  24501  clwlkiswlk  25161  sspnv  26039  lnof  26070  bloln  26099  reff  28281  signsply0  29000  cvmliftmolem1  29565  cvmlift2lem9a  29587  mbfresfi  31413  itg2gt0cn  31423  ismtyres  31566  ghomf  31606  rngoisohom  31645  pridlidl  31694  pridlnr  31695  maxidlidl  31700  lflf  32061  lkrcl  32090  cvrlt  32268  cvrle  32276  atbase  32287  llnbase  32506  lplnbase  32531  lvolbase  32575  psubssat  32751  lhpbase  32995  laut1o  33082  ldillaut  33108  ltrnldil  33119  diadmclN  34037  pell1234qrre  35129  lnmlsslnm  35369  cvgdvgrat  36022  stoweidlem34  37165
  Copyright terms: Public domain W3C validator