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

Theorem simplbda 501
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 478 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 497 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 398
This theorem is referenced by:  cantnflem3  9561  fseqenlem2  9895  axdc3lem2  10321  fpwwe2lem11  10511  rlimsqzlem  15468  ramub1lem2  16834  invfun  17582  pltne  18158  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  oppnid  27474  sspba  29455  sspg  29456  ssps  29458  sspn  29464  nmblore  29514  phpar  29552  ocorth  30019  elnlfn2  30657  foresf1o  31216  fnpreimac  31372  fpwrelmap  31432  kerunit  31895  0nellinds  31940  linds2eq  31949  rhmpreimaidl  31977  rhmpreimaprmidl  32001  lindsunlem  32090  dimkerim  32093  reff  32181  cnre2csqlem  32252  fmcncfil  32273  elzrhunit  32321  qqhval2lem  32323  baselsiga  32475  signsply0  32924  cvmliftmolem1  33636  mclsppslem  33938  mclspps  33939  cofcutr  34232  fnetr  34709  relowlssretop  35720  mbfresfi  36010  itg2addnclem  36015  itg2addnclem2  36016  sstotbnd2  36119  rngoiso1o  36324  pridl  36382  lfli  37409  lkrf0  37441  cvrne  37629  atcvr0  37636  psubspi  38096  psubcli2N  38288  lhp1cvr  38348  lautle  38433  diadmleN  39387  cvgdvgrat  42326  radcnvrat  42327  projf1o  43137  islptre  43570  islpcn  43590  icccncfext  43838  fdivmptf  46327  refdivmptf  46328  rege1logbrege0  46344
  Copyright terms: Public domain W3C validator