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

Theorem simprbda 633
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 491 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simpld 465 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  elrabi  3204  oteqex  4707  fsnex  6205  fisupg  7844  fiinfg  8040  cantnff  8204  fseqenlem2  8481  fpwwe2lem11  9090  fpwwe2lem12  9091  fpwwe2  9093  rlimsqzlem  13760  ramub1lem2  15033  mriss  15589  invfun  15717  pltle  16255  subgslw  17316  frgpnabllem2  17558  cyggeninv  17566  ablfaclem3  17768  psrbagf  18637  mplind  18773  pjff  19323  pjf2  19325  pjfo  19326  pjcss  19327  fvmptnn04ifc  19924  chfacfisf  19926  chfacfisfcpmat  19927  tg1  20027  cldss  20092  cnf2  20313  cncnp  20344  lly1stc  20559  refbas  20573  qtoptop2  20762  qtoprest  20780  elfm3  21013  flfelbas  21057  cnextf  21129  restutopopn  21301  cfilufbas  21352  fmucnd  21355  blgt0  21462  xblss2ps  21464  xblss2  21465  tngngp  21710  cfilfil  22285  iscau2  22295  caufpm  22300  cmetcaulem  22306  dvcnp2  22922  dvfsumrlim  23031  dvfsumrlim2  23032  fta1g  23166  dvdsflsumcom  24165  fsumvma  24189  vmadivsumb  24369  dchrisumlema  24374  dchrvmasumlem1  24381  dchrvmasum2lem  24382  dchrvmasumiflem1  24387  selbergb  24435  selberg2b  24438  pntibndlem3  24478  pntlem3  24495  motgrp  24636  oppnid  24836  clwlkiswlk  25533  sspnv  26413  lnof  26444  bloln  26473  reff  28714  signsply0  29488  cvmliftmolem1  30052  cvmlift2lem9a  30074  mbfresfi  32031  itg2gt0cn  32041  ismtyres  32184  ghomf  32224  rngoisohom  32263  pridlidl  32312  pridlnr  32313  maxidlidl  32318  lflf  32673  lkrcl  32702  cvrlt  32880  cvrle  32888  atbase  32899  llnbase  33118  lplnbase  33143  lvolbase  33187  psubssat  33363  lhpbase  33607  laut1o  33694  ldillaut  33720  ltrnldil  33731  diadmclN  34649  pell1234qrre  35742  lnmlsslnm  35983  cvgdvgrat  36705  stoweidlem34  37932
  Copyright terms: Public domain W3C validator