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  3240  oteqex  4730  fisupg  7770  cantnff  8096  fseqenlem2  8409  fpwwe2lem11  9021  fpwwe2lem12  9022  fpwwe2  9024  rlimsqzlem  13453  ramub1lem2  14527  mriss  15014  invfun  15140  pltle  15570  subgslw  16615  frgpnabllem2  16857  cyggeninv  16865  ablfaclem3  17117  psrbagf  17993  mplind  18146  pjff  18721  pjf2  18723  pjfo  18724  pjcss  18725  fvmptnn04ifc  19331  chfacfisf  19333  chfacfisfcpmat  19334  tg1  19443  cldss  19508  cnf2  19728  cncnp  19759  lly1stc  19975  refbas  19989  qtoptop2  20178  qtoprest  20196  elfm3  20429  flfelbas  20473  cnextf  20544  restutopopn  20719  cfilufbas  20770  fmucnd  20773  blgt0  20880  xblss2ps  20882  xblss2  20883  tngngp  21146  cfilfil  21684  iscau2  21694  caufpm  21699  cmetcaulem  21705  dvcnp2  22301  dvfsumrlim  22410  dvfsumrlim2  22411  fta1g  22546  dvdsflsumcom  23442  fsumvma  23466  vmadivsumb  23646  dchrisumlema  23651  dchrvmasumlem1  23658  dchrvmasum2lem  23659  dchrvmasumiflem1  23664  selbergb  23712  selberg2b  23715  pntibndlem3  23755  pntlem3  23772  motgrp  23908  oppnid  24096  clwlkiswlk  24735  sspnv  25617  lnof  25648  bloln  25677  reff  27820  signsply0  28486  cvmliftmolem1  28704  cvmlift2lem9a  28726  mbfresfi  30037  itg2gt0cn  30046  ismtyres  30280  ghomf  30320  rngoisohom  30359  pridlidl  30408  pridlnr  30409  maxidlidl  30414  pell1234qrre  30764  lnmlsslnm  31003  cvgdvgrat  31170  stoweidlem34  31770  lflf  34663  lkrcl  34692  cvrlt  34870  cvrle  34878  atbase  34889  llnbase  35108  lplnbase  35133  lvolbase  35177  psubssat  35353  lhpbase  35597  laut1o  35684  ldillaut  35710  ltrnldil  35721  diadmclN  36639
  Copyright terms: Public domain W3C validator