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

Theorem simplbda 608
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
Hypothesis
Ref Expression
pm3.26bda.1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
simplbda  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem simplbda
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 471 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 450 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  cantnflem3  7639  mapfien  7645  fseqenlem2  7898  axdc3lem2  8323  fpwwe2lem12  8508  rlimsqzlem  12434  ramub1lem2  13387  invfun  13981  pltne  14411  cntzi  15120  odmulg  15184  subgslw  15242  frgpnabllem1  15476  cyggeninv  15485  ablfaclem3  15637  lsslmod  16028  pjff  16931  pjf2  16933  pjcss  16935  ocvpj  16936  tgcl  17026  cldopn  17087  cncnp  17336  1stcelcls  17516  lly1stc  17551  qtoptop2  17723  qtopid  17729  trfg  17915  flfneii  18016  fclsbas  18045  isfcf  18058  restutop  18259  restutopopn  18260  cfiluexsm  18312  cfilufg  18315  blgt0  18421  xblss2ps  18423  xblss2  18424  mopni  18514  metrest  18546  metustblOLD  18602  metustbl  18603  restmetu  18609  cfilss  19215  caun0  19226  cmetcaulem  19233  cfilresi  19240  cmetcuspOLD  19299  cnlimci  19768  dvcl  19778  dvcnp  19797  dvcnp2  19798  dvnadd  19807  dvfsumrlimge0  19906  dvfsumrlim  19907  dvfsumrlim2  19908  evlslem3  19927  fta1g  20082  plyeq0lem  20121  vieta1lem1  20219  vieta1lem2  20220  fsumharmonic  20842  dvdsflf1o  20964  dvdsflsumcom  20965  fsumvma  20989  vmadivsumb  21169  dchrisum0lem1a  21172  dchrisumlema  21174  dchrisumlem3  21177  dchrmusum2  21180  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  dchrisum0fno1  21197  dchrisum0lem1b  21201  mulog2sumlem2  21221  vmalogdivsum2  21224  2vmadivsumlem  21226  selberglem2  21232  selbergb  21235  selberg2b  21238  selberg3lem1  21243  selberg4lem1  21246  pntpbnd1  21272  pntibndlem3  21278  pntlem3  21295  sspba  22218  sspg  22219  ssps  22221  sspn  22227  nmblore  22279  phpar  22317  ocorth  22785  elnlfn2  23424  kerunit  24253  cnre2csqlem  24300  fmcncfil  24309  elzrhunit  24355  qqhval2lem  24357  baselsiga  24490  cvmliftmolem1  24960  mbfresfi  26243  itg2addnclem  26246  itg2addnclem2  26247  refssex  26352  fnetr  26357  sstotbnd2  26474  rngoiso1o  26586  pridl  26638  lfli  29796  lkrf0  29828  cvrne  30016  atcvr0  30023  psubspi  30481  psubcli2N  30673  lhp1cvr  30733  lautle  30818  diadmleN  31773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator