Theorem simplbda 499

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simplbda	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 495	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cantnflem3  9612  fseqenlem2  9947  axdc3lem2  10373  fpwwe2lem11  10564  rlimsqzlem  15611  ramub1lem2  16998  invfun  17731  pltne  18298  cntzi  19304  odmulg  19531  subgslw  19591  frgpnabllem1  19848  cyggeninv  19858  ablfaclem3  20064  lsslmod  20955  rhmpreimaidl  21275  psgnevpm  21569  pjff  21692  pjf2  21694  pjcss  21696  ocvpj  21697  evlslem3  22058  mhpdeg  22111  scmatscmid  22471  fvmptnn04ifc  22817  fvmptnn04ifd  22818  tgcl  22934  cldopn  22996  cncnp  23245  1stcelcls  23426  lly1stc  23461  refssex  23476  qtoptop2  23664  qtopid  23670  trfg  23856  flfneii  23957  fclsbas  23986  isfcf  23999  restutop  24202  restutopopn  24203  isucn2  24243  cfiluexsm  24254  cfilufg  24257  blgt0  24364  xblss2ps  24366  xblss2  24367  mopni  24457  metrest  24489  metustbl  24531  restmetu  24535  cfilss  25237  caun0  25248  cmetcaulem  25255  cfilresi  25262  cmetcusp  25321  cnlimci  25856  dvcl  25866  dvcnp  25886  dvcnp2  25887  dvnadd  25896  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsumrlim2  25999  fta1g  26135  plyeq0lem  26175  vieta1lem1  26276  vieta1lem2  26277  fsumharmonic  26975  dvdsflf1o  27150  dvdsflsumcom  27151  fsumvma  27176  vmadivsumb  27446  dchrisum0lem1a  27449  dchrisumlema  27451  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0fno1  27474  dchrisum0lem1b  27478  mulog2sumlem2  27498  vmalogdivsum2  27501  2vmadivsumlem  27503  selberglem2  27509  selbergb  27512  selberg2b  27515  selberg3lem1  27520  selberg4lem1  27523  pntpbnd1  27549  pntibndlem3  27555  pntlem3  27572  sltsleft  27852  sltsright  27853  cofcutr  27916  oppnid  28814  sspba  30798  sspg  30799  ssps  30801  sspn  30807  nmblore  30857  phpar  30895  ocorth  31362  elnlfn2  32000  foresf1o  32574  fnpreimac  32743  fpwrelmap  32806  elrgspnsubrunlem2  33309  kerunit  33385  0nellinds  33430  linds2eq  33441  dvdsruasso  33445  unitpidl1  33484  rhmpreimaprmidl  33511  mxidlirredi  33531  rprmdvds  33579  rprmnz  33580  1arithufdlem3  33606  ply1unit  33635  ply1degltlss  33656  esplyfvaln  33718  exsslsb  33741  ply1degltdimlem  33766  lindsunlem  33768  dimkerim  33771  irngss  33831  0ringirng  33833  irngnminplynz  33856  algextdeglem8  33868  reff  33983  cnre2csqlem  34054  fmcncfil  34075  elzrhunit  34121  qqhval2lem  34125  baselsiga  34259  signsply0  34695  cvmliftmolem1  35463  mclsppslem  35765  mclspps  35766  fnetr  36533  relowlssretop  37679  mbfresfi  37987  itg2addnclem  37992  itg2addnclem2  37993  sstotbnd2  38095  rngoiso1o  38300  pridl  38358  lfli  39507  lkrf0  39539  cvrne  39727  atcvr0  39734  psubspi  40193  psubcli2N  40385  lhp1cvr  40445  lautle  40530  diadmleN  41484  sn-eluzp1l  42740  cvgdvgrat  44740  radcnvrat  44741  projf1o  45626  islptre  46049  islpcn  46067  icccncfext  46315  fdivmptf  49011  refdivmptf  49012  rege1logbrege0  49028  nelsubc2  49538  termcterm2  49983