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

Theorem simplbda 651
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
Hypothesis
Ref Expression
pm3.26bda.1 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Assertion
Ref Expression
simplbda ((𝜑𝜓) → 𝜃)

Proof of Theorem simplbda
StepHypRef Expression
1 pm3.26bda.1 . . 3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
21biimpa 499 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 477 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  cantnflem3  8449  fseqenlem2  8709  axdc3lem2  9134  fpwwe2lem12  9320  rlimsqzlem  14176  ramub1lem2  15518  invfun  16196  pltne  16734  cntzi  17534  odmulg  17745  subgslw  17803  frgpnabllem1  18048  cyggeninv  18057  ablfaclem3  18258  lsslmod  18730  evlslem3  19284  psgnevpm  19702  pjff  19823  pjf2  19825  pjcss  19827  ocvpj  19828  scmatscmid  20079  fvmptnn04ifc  20424  fvmptnn04ifd  20425  tgcl  20532  cldopn  20593  cncnp  20842  1stcelcls  21022  lly1stc  21057  refssex  21072  qtoptop2  21260  qtopid  21266  trfg  21453  flfneii  21554  fclsbas  21583  isfcf  21596  restutop  21799  restutopopn  21800  isucn2  21841  cfiluexsm  21852  cfilufg  21855  blgt0  21962  xblss2ps  21964  xblss2  21965  mopni  22055  metrest  22087  metustbl  22129  restmetu  22133  cfilss  22821  caun0  22832  cmetcaulem  22839  cfilresi  22846  cmetcusp  22903  cnlimci  23404  dvcl  23414  dvcnp  23433  dvcnp2  23434  dvnadd  23443  dvfsumrlimge0  23542  dvfsumrlim  23543  dvfsumrlim2  23544  fta1g  23676  plyeq0lem  23715  vieta1lem1  23814  vieta1lem2  23815  fsumharmonic  24483  dvdsflf1o  24658  dvdsflsumcom  24659  fsumvma  24683  vmadivsumb  24917  dchrisum0lem1a  24920  dchrisumlema  24922  dchrisumlem3  24925  dchrmusum2  24928  dchrvmasumlem2  24932  dchrvmasumiflem1  24935  dchrisum0fno1  24945  dchrisum0lem1b  24949  mulog2sumlem2  24969  vmalogdivsum2  24972  2vmadivsumlem  24974  selberglem2  24980  selbergb  24983  selberg2b  24986  selberg3lem1  24991  selberg4lem1  24994  pntpbnd1  25020  pntibndlem3  25026  pntlem3  25043  oppnid  25384  sspba  26798  sspg  26799  ssps  26801  sspn  26807  nmblore  26859  phpar  26897  ocorth  27368  elnlfn2  28006  foresf1o  28561  fpwrelmap  28730  kerunit  28988  reff  29068  cnre2csqlem  29118  fmcncfil  29139  elzrhunit  29185  qqhval2lem  29187  baselsiga  29339  signsply0  29788  cvmliftmolem1  30351  mclsppslem  30568  mclspps  30569  fnetr  31350  relowlssretop  32211  mbfresfi  32450  itg2addnclem  32455  itg2addnclem2  32456  sstotbnd2  32567  rngoiso1o  32772  pridl  32830  lfli  33190  lkrf0  33222  cvrne  33410  atcvr0  33417  psubspi  33875  psubcli2N  34067  lhp1cvr  34127  lautle  34212  diadmleN  35169  cvgdvgrat  37358  radcnvrat  37359  islptre  38510  islpcn  38530  icccncfext  38597  fdivmptf  42155  refdivmptf  42156  rege1logbrege0  42172
  Copyright terms: Public domain W3C validator