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

Theorem simplbda 503
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 480 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 499 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  cantnflem3  9138  fseqenlem2  9436  axdc3lem2  9862  fpwwe2lem12  10052  rlimsqzlem  14997  ramub1lem2  16353  invfun  17026  pltne  17564  cntzi  18451  odmulg  18675  subgslw  18733  frgpnabllem1  18986  cyggeninv  18995  ablfaclem3  19202  lsslmod  19725  psgnevpm  20278  pjff  20401  pjf2  20403  pjcss  20405  ocvpj  20406  evlslem3  20752  mhpdeg  20796  scmatscmid  21111  fvmptnn04ifc  21457  fvmptnn04ifd  21458  tgcl  21574  cldopn  21636  cncnp  21885  1stcelcls  22066  lly1stc  22101  refssex  22116  qtoptop2  22304  qtopid  22310  trfg  22496  flfneii  22597  fclsbas  22626  isfcf  22639  restutop  22843  restutopopn  22844  isucn2  22885  cfiluexsm  22896  cfilufg  22899  blgt0  23006  xblss2ps  23008  xblss2  23009  mopni  23099  metrest  23131  metustbl  23173  restmetu  23177  cfilss  23874  caun0  23885  cmetcaulem  23892  cfilresi  23899  cmetcusp  23958  cnlimci  24492  dvcl  24502  dvcnp  24522  dvcnp2  24523  dvnadd  24532  dvfsumrlimge0  24633  dvfsumrlim  24634  dvfsumrlim2  24635  fta1g  24768  plyeq0lem  24807  vieta1lem1  24906  vieta1lem2  24907  fsumharmonic  25597  dvdsflf1o  25772  dvdsflsumcom  25773  fsumvma  25797  vmadivsumb  26067  dchrisum0lem1a  26070  dchrisumlema  26072  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  dchrisum0fno1  26095  dchrisum0lem1b  26099  mulog2sumlem2  26119  vmalogdivsum2  26122  2vmadivsumlem  26124  selberglem2  26130  selbergb  26133  selberg2b  26136  selberg3lem1  26141  selberg4lem1  26144  pntpbnd1  26170  pntibndlem3  26176  pntlem3  26193  oppnid  26540  sspba  28510  sspg  28511  ssps  28513  sspn  28519  nmblore  28569  phpar  28607  ocorth  29074  elnlfn2  29712  foresf1o  30273  fnpreimac  30434  fpwrelmap  30495  kerunit  30947  0nellinds  30986  linds2eq  30995  rhmpreimaidl  31011  rhmpreimaprmidl  31035  lindsunlem  31108  dimkerim  31111  reff  31192  cnre2csqlem  31263  fmcncfil  31284  elzrhunit  31330  qqhval2lem  31332  baselsiga  31484  signsply0  31931  cvmliftmolem1  32638  mclsppslem  32940  mclspps  32941  fnetr  33809  relowlssretop  34777  mbfresfi  35100  itg2addnclem  35105  itg2addnclem2  35106  sstotbnd2  35209  rngoiso1o  35414  pridl  35472  lfli  36354  lkrf0  36386  cvrne  36574  atcvr0  36581  psubspi  37040  psubcli2N  37232  lhp1cvr  37292  lautle  37377  diadmleN  38331  cvgdvgrat  41012  radcnvrat  41013  projf1o  41820  islptre  42256  islpcn  42276  icccncfext  42524  fdivmptf  44950  refdivmptf  44951  rege1logbrege0  44967
  Copyright terms: Public domain W3C validator