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  9586  fseqenlem2  9920  axdc3lem2  10346  fpwwe2lem11  10536  rlimsqzlem  15493  ramub1lem2  16859  invfun  17607  pltne  18183  cntzi  19068  odmulg  19297  subgslw  19357  frgpnabllem1  19610  cyggeninv  19619  ablfaclem3  19825  lsslmod  20374  psgnevpm  20946  pjff  21071  pjf2  21073  pjcss  21075  ocvpj  21076  evlslem3  21442  mhpdeg  21487  scmatscmid  21807  fvmptnn04ifc  22153  fvmptnn04ifd  22154  tgcl  22271  cldopn  22334  cncnp  22583  1stcelcls  22764  lly1stc  22799  refssex  22814  qtoptop2  23002  qtopid  23008  trfg  23194  flfneii  23295  fclsbas  23324  isfcf  23337  restutop  23541  restutopopn  23542  isucn2  23583  cfiluexsm  23594  cfilufg  23597  blgt0  23704  xblss2ps  23706  xblss2  23707  mopni  23800  metrest  23832  metustbl  23874  restmetu  23878  cfilss  24586  caun0  24597  cmetcaulem  24604  cfilresi  24611  cmetcusp  24670  cnlimci  25205  dvcl  25215  dvcnp  25235  dvcnp2  25236  dvnadd  25245  dvfsumrlimge0  25346  dvfsumrlim  25347  dvfsumrlim2  25348  fta1g  25484  plyeq0lem  25523  vieta1lem1  25622  vieta1lem2  25623  fsumharmonic  26313  dvdsflf1o  26488  dvdsflsumcom  26489  fsumvma  26513  vmadivsumb  26783  dchrisum0lem1a  26786  dchrisumlema  26788  dchrisumlem3  26791  dchrmusum2  26794  dchrvmasumlem2  26798  dchrvmasumiflem1  26801  dchrisum0fno1  26811  dchrisum0lem1b  26815  mulog2sumlem2  26835  vmalogdivsum2  26838  2vmadivsumlem  26840  selberglem2  26846  selbergb  26849  selberg2b  26852  selberg3lem1  26857  selberg4lem1  26860  pntpbnd1  26886  pntibndlem3  26892  pntlem3  26909  ssltleft  27152  ssltright  27153  cofcutr  27192  oppnid  27517  sspba  29498  sspg  29499  ssps  29501  sspn  29507  nmblore  29557  phpar  29595  ocorth  30062  elnlfn2  30700  foresf1o  31259  fnpreimac  31415  fpwrelmap  31475  kerunit  31938  0nellinds  31983  linds2eq  31992  rhmpreimaidl  32020  rhmpreimaprmidl  32044  lindsunlem  32133  dimkerim  32136  reff  32224  cnre2csqlem  32295  fmcncfil  32316  elzrhunit  32364  qqhval2lem  32366  baselsiga  32518  signsply0  32967  cvmliftmolem1  33679  mclsppslem  33981  mclspps  33982  fnetr  34755  relowlssretop  35766  mbfresfi  36056  itg2addnclem  36061  itg2addnclem2  36062  sstotbnd2  36165  rngoiso1o  36370  pridl  36428  lfli  37455  lkrf0  37487  cvrne  37675  atcvr0  37682  psubspi  38142  psubcli2N  38334  lhp1cvr  38394  lautle  38479  diadmleN  39433  cvgdvgrat  42498  radcnvrat  42499  projf1o  43316  islptre  43755  islpcn  43775  icccncfext  44023  fdivmptf  46522  refdivmptf  46523  rege1logbrege0  46539
  Copyright terms: Public domain W3C validator