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

Theorem simplbda 655
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 502 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 482 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  cantnflem3  8753  fseqenlem2  9030  axdc3lem2  9457  fpwwe2lem12  9647  rlimsqzlem  14570  ramub1lem2  15925  invfun  16617  pltne  17155  cntzi  17954  odmulg  18165  subgslw  18223  frgpnabllem1  18468  cyggeninv  18477  ablfaclem3  18678  lsslmod  19154  evlslem3  19708  psgnevpm  20129  pjff  20250  pjf2  20252  pjcss  20254  ocvpj  20255  scmatscmid  20506  fvmptnn04ifc  20851  fvmptnn04ifd  20852  tgcl  20967  cldopn  21029  cncnp  21278  1stcelcls  21458  lly1stc  21493  refssex  21508  qtoptop2  21696  qtopid  21702  trfg  21888  flfneii  21989  fclsbas  22018  isfcf  22031  restutop  22234  restutopopn  22235  isucn2  22276  cfiluexsm  22287  cfilufg  22290  blgt0  22397  xblss2ps  22399  xblss2  22400  mopni  22490  metrest  22522  metustbl  22564  restmetu  22568  cfilss  23260  caun0  23271  cmetcaulem  23278  cfilresi  23285  cmetcusp  23342  cnlimci  23844  dvcl  23854  dvcnp  23873  dvcnp2  23874  dvnadd  23883  dvfsumrlimge0  23984  dvfsumrlim  23985  dvfsumrlim2  23986  fta1g  24118  plyeq0lem  24157  vieta1lem1  24256  vieta1lem2  24257  fsumharmonic  24929  dvdsflf1o  25104  dvdsflsumcom  25105  fsumvma  25129  vmadivsumb  25363  dchrisum0lem1a  25366  dchrisumlema  25368  dchrisumlem3  25371  dchrmusum2  25374  dchrvmasumlem2  25378  dchrvmasumiflem1  25381  dchrisum0fno1  25391  dchrisum0lem1b  25395  mulog2sumlem2  25415  vmalogdivsum2  25418  2vmadivsumlem  25420  selberglem2  25426  selbergb  25429  selberg2b  25432  selberg3lem1  25437  selberg4lem1  25440  pntpbnd1  25466  pntibndlem3  25472  pntlem3  25489  oppnid  25829  sspba  27883  sspg  27884  ssps  27886  sspn  27892  nmblore  27942  phpar  27980  ocorth  28451  elnlfn2  29089  foresf1o  29642  fpwrelmap  29809  kerunit  30124  reff  30207  cnre2csqlem  30257  fmcncfil  30278  elzrhunit  30324  qqhval2lem  30326  baselsiga  30479  signsply0  30929  cvmliftmolem1  31562  mclsppslem  31779  mclspps  31780  fnetr  32644  relowlssretop  33514  mbfresfi  33761  itg2addnclem  33766  itg2addnclem2  33767  sstotbnd2  33878  rngoiso1o  34083  pridl  34141  lfli  34843  lkrf0  34875  cvrne  35063  atcvr0  35070  psubspi  35528  psubcli2N  35720  lhp1cvr  35780  lautle  35865  diadmleN  36821  cvgdvgrat  39006  radcnvrat  39007  islptre  40346  islpcn  40366  icccncfext  40595  fdivmptf  42837  refdivmptf  42838  rege1logbrege0  42854
  Copyright terms: Public domain W3C validator