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  9576  fseqenlem2  9908  axdc3lem2  10334  fpwwe2lem11  10524  rlimsqzlem  15548  ramub1lem2  16931  invfun  17663  pltne  18230  cntzi  19234  odmulg  19461  subgslw  19521  frgpnabllem1  19778  cyggeninv  19788  ablfaclem3  19994  lsslmod  20886  rhmpreimaidl  21207  psgnevpm  21519  pjff  21642  pjf2  21644  pjcss  21646  ocvpj  21647  evlslem3  22008  mhpdeg  22053  scmatscmid  22414  fvmptnn04ifc  22760  fvmptnn04ifd  22761  tgcl  22877  cldopn  22939  cncnp  23188  1stcelcls  23369  lly1stc  23404  refssex  23419  qtoptop2  23607  qtopid  23613  trfg  23799  flfneii  23900  fclsbas  23929  isfcf  23942  restutop  24145  restutopopn  24146  isucn2  24186  cfiluexsm  24197  cfilufg  24200  blgt0  24307  xblss2ps  24309  xblss2  24310  mopni  24400  metrest  24432  metustbl  24474  restmetu  24478  cfilss  25190  caun0  25201  cmetcaulem  25208  cfilresi  25215  cmetcusp  25274  cnlimci  25810  dvcl  25820  dvcnp  25840  dvcnp2  25841  dvcnp2OLD  25842  dvnadd  25851  dvfsumrlimge0  25957  dvfsumrlim  25958  dvfsumrlim2  25959  fta1g  26095  plyeq0lem  26135  vieta1lem1  26238  vieta1lem2  26239  fsumharmonic  26942  dvdsflf1o  27117  dvdsflsumcom  27118  fsumvma  27144  vmadivsumb  27414  dchrisum0lem1a  27417  dchrisumlema  27419  dchrisumlem3  27422  dchrmusum2  27425  dchrvmasumlem2  27429  dchrvmasumiflem1  27432  dchrisum0fno1  27442  dchrisum0lem1b  27446  mulog2sumlem2  27466  vmalogdivsum2  27469  2vmadivsumlem  27471  selberglem2  27477  selbergb  27480  selberg2b  27483  selberg3lem1  27488  selberg4lem1  27491  pntpbnd1  27517  pntibndlem3  27523  pntlem3  27540  ssltleft  27808  ssltright  27809  cofcutr  27861  oppnid  28717  sspba  30697  sspg  30698  ssps  30700  sspn  30706  nmblore  30756  phpar  30794  ocorth  31261  elnlfn2  31899  foresf1o  32474  fnpreimac  32643  fpwrelmap  32706  elrgspnsubrunlem2  33205  kerunit  33280  0nellinds  33325  linds2eq  33336  dvdsruasso  33340  unitpidl1  33379  rhmpreimaprmidl  33406  mxidlirredi  33426  rprmdvds  33474  rprmnz  33475  1arithufdlem3  33501  ply1unit  33528  ply1degltlss  33547  exsslsb  33599  ply1degltdimlem  33625  lindsunlem  33627  dimkerim  33630  irngss  33690  0ringirng  33692  irngnminplynz  33715  algextdeglem8  33727  reff  33842  cnre2csqlem  33913  fmcncfil  33934  elzrhunit  33980  qqhval2lem  33984  baselsiga  34118  signsply0  34554  cvmliftmolem1  35293  mclsppslem  35595  mclspps  35596  fnetr  36364  relowlssretop  37376  mbfresfi  37685  itg2addnclem  37690  itg2addnclem2  37691  sstotbnd2  37793  rngoiso1o  37998  pridl  38056  lfli  39079  lkrf0  39111  cvrne  39299  atcvr0  39306  psubspi  39765  psubcli2N  39957  lhp1cvr  40017  lautle  40102  diadmleN  41056  sn-eluzp1l  42320  cvgdvgrat  44325  radcnvrat  44326  projf1o  45213  islptre  45638  islpcn  45656  icccncfext  45904  fdivmptf  48552  refdivmptf  48553  rege1logbrege0  48569  nelsubc2  49080  termcterm2  49525