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

Theorem simplbda 500
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 477 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 496 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 206  df-an 397
This theorem is referenced by:  cantnflem3  9560  fseqenlem2  9894  axdc3lem2  10320  fpwwe2lem11  10510  rlimsqzlem  15467  ramub1lem2  16833  invfun  17581  pltne  18157  cntzi  19041  odmulg  19269  subgslw  19327  frgpnabllem1  19580  cyggeninv  19589  ablfaclem3  19795  lsslmod  20344  psgnevpm  20916  pjff  21041  pjf2  21043  pjcss  21045  ocvpj  21046  evlslem3  21412  mhpdeg  21457  scmatscmid  21777  fvmptnn04ifc  22123  fvmptnn04ifd  22124  tgcl  22241  cldopn  22304  cncnp  22553  1stcelcls  22734  lly1stc  22769  refssex  22784  qtoptop2  22972  qtopid  22978  trfg  23164  flfneii  23265  fclsbas  23294  isfcf  23307  restutop  23511  restutopopn  23512  isucn2  23553  cfiluexsm  23564  cfilufg  23567  blgt0  23674  xblss2ps  23676  xblss2  23677  mopni  23770  metrest  23802  metustbl  23844  restmetu  23848  cfilss  24556  caun0  24567  cmetcaulem  24574  cfilresi  24581  cmetcusp  24640  cnlimci  25175  dvcl  25185  dvcnp  25205  dvcnp2  25206  dvnadd  25215  dvfsumrlimge0  25316  dvfsumrlim  25317  dvfsumrlim2  25318  fta1g  25454  plyeq0lem  25493  vieta1lem1  25592  vieta1lem2  25593  fsumharmonic  26283  dvdsflf1o  26458  dvdsflsumcom  26459  fsumvma  26483  vmadivsumb  26753  dchrisum0lem1a  26756  dchrisumlema  26758  dchrisumlem3  26761  dchrmusum2  26764  dchrvmasumlem2  26768  dchrvmasumiflem1  26771  dchrisum0fno1  26781  dchrisum0lem1b  26785  mulog2sumlem2  26805  vmalogdivsum2  26808  2vmadivsumlem  26810  selberglem2  26816  selbergb  26819  selberg2b  26822  selberg3lem1  26827  selberg4lem1  26830  pntpbnd1  26856  pntibndlem3  26862  pntlem3  26879  ssltleft  27121  ssltright  27122  cofcutr  27161  oppnid  27486  sspba  29467  sspg  29468  ssps  29470  sspn  29476  nmblore  29526  phpar  29564  ocorth  30031  elnlfn2  30669  foresf1o  31228  fnpreimac  31384  fpwrelmap  31444  kerunit  31907  0nellinds  31952  linds2eq  31961  rhmpreimaidl  31989  rhmpreimaprmidl  32013  lindsunlem  32102  dimkerim  32105  reff  32193  cnre2csqlem  32264  fmcncfil  32285  elzrhunit  32333  qqhval2lem  32335  baselsiga  32487  signsply0  32936  cvmliftmolem1  33648  mclsppslem  33950  mclspps  33951  fnetr  34718  relowlssretop  35729  mbfresfi  36019  itg2addnclem  36024  itg2addnclem2  36025  sstotbnd2  36128  rngoiso1o  36333  pridl  36391  lfli  37418  lkrf0  37450  cvrne  37638  atcvr0  37645  psubspi  38105  psubcli2N  38297  lhp1cvr  38357  lautle  38442  diadmleN  39396  cvgdvgrat  42357  radcnvrat  42358  projf1o  43174  islptre  43613  islpcn  43633  icccncfext  43881  fdivmptf  46376  refdivmptf  46377  rege1logbrege0  46393
  Copyright terms: Public domain W3C validator