Theorem simplbda 499

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

Step	Hyp	Ref	Expression
1		pm3.26bda.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  9600  fseqenlem2  9935  axdc3lem2  10361  fpwwe2lem11  10552  rlimsqzlem  15572  ramub1lem2  16955  invfun  17688  pltne  18255  cntzi  19258  odmulg  19485  subgslw  19545  frgpnabllem1  19802  cyggeninv  19812  ablfaclem3  20018  lsslmod  20911  rhmpreimaidl  21232  psgnevpm  21544  pjff  21667  pjf2  21669  pjcss  21671  ocvpj  21672  evlslem3  22035  mhpdeg  22088  scmatscmid  22450  fvmptnn04ifc  22796  fvmptnn04ifd  22797  tgcl  22913  cldopn  22975  cncnp  23224  1stcelcls  23405  lly1stc  23440  refssex  23455  qtoptop2  23643  qtopid  23649  trfg  23835  flfneii  23936  fclsbas  23965  isfcf  23978  restutop  24181  restutopopn  24182  isucn2  24222  cfiluexsm  24233  cfilufg  24236  blgt0  24343  xblss2ps  24345  xblss2  24346  mopni  24436  metrest  24468  metustbl  24510  restmetu  24514  cfilss  25226  caun0  25237  cmetcaulem  25244  cfilresi  25251  cmetcusp  25310  cnlimci  25846  dvcl  25856  dvcnp  25876  dvcnp2  25877  dvcnp2OLD  25878  dvnadd  25887  dvfsumrlimge0  25993  dvfsumrlim  25994  dvfsumrlim2  25995  fta1g  26131  plyeq0lem  26171  vieta1lem1  26274  vieta1lem2  26275  fsumharmonic  26978  dvdsflf1o  27153  dvdsflsumcom  27154  fsumvma  27180  vmadivsumb  27450  dchrisum0lem1a  27453  dchrisumlema  27455  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0fno1  27478  dchrisum0lem1b  27482  mulog2sumlem2  27502  vmalogdivsum2  27505  2vmadivsumlem  27507  selberglem2  27513  selbergb  27516  selberg2b  27519  selberg3lem1  27524  selberg4lem1  27527  pntpbnd1  27553  pntibndlem3  27559  pntlem3  27576  sltsleft  27856  sltsright  27857  cofcutr  27920  oppnid  28818  sspba  30802  sspg  30803  ssps  30805  sspn  30811  nmblore  30861  phpar  30899  ocorth  31366  elnlfn2  32004  foresf1o  32579  fnpreimac  32749  fpwrelmap  32812  elrgspnsubrunlem2  33330  kerunit  33406  0nellinds  33451  linds2eq  33462  dvdsruasso  33466  unitpidl1  33505  rhmpreimaprmidl  33532  mxidlirredi  33552  rprmdvds  33600  rprmnz  33601  1arithufdlem3  33627  ply1unit  33656  ply1degltlss  33677  exsslsb  33753  ply1degltdimlem  33779  lindsunlem  33781  dimkerim  33784  irngss  33844  0ringirng  33846  irngnminplynz  33869  algextdeglem8  33881  reff  33996  cnre2csqlem  34067  fmcncfil  34088  elzrhunit  34134  qqhval2lem  34138  baselsiga  34272  signsply0  34708  cvmliftmolem1  35475  mclsppslem  35777  mclspps  35778  fnetr  36545  relowlssretop  37564  mbfresfi  37863  itg2addnclem  37868  itg2addnclem2  37869  sstotbnd2  37971  rngoiso1o  38176  pridl  38234  lfli  39317  lkrf0  39349  cvrne  39537  atcvr0  39544  psubspi  40003  psubcli2N  40195  lhp1cvr  40255  lautle  40340  diadmleN  41294  sn-eluzp1l  42559  cvgdvgrat  44550  radcnvrat  44551  projf1o  45437  islptre  45861  islpcn  45879  icccncfext  46127  fdivmptf  48783  refdivmptf  48784  rege1logbrege0  48800  nelsubc2  49310  termcterm2  49755