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  9703  fseqenlem2  10037  axdc3lem2  10463  fpwwe2lem11  10653  rlimsqzlem  15663  ramub1lem2  17045  invfun  17775  pltne  18342  cntzi  19310  odmulg  19535  subgslw  19595  frgpnabllem1  19852  cyggeninv  19862  ablfaclem3  20068  lsslmod  20915  rhmpreimaidl  21236  psgnevpm  21547  pjff  21670  pjf2  21672  pjcss  21674  ocvpj  21675  evlslem3  22036  mhpdeg  22081  scmatscmid  22442  fvmptnn04ifc  22788  fvmptnn04ifd  22789  tgcl  22905  cldopn  22967  cncnp  23216  1stcelcls  23397  lly1stc  23432  refssex  23447  qtoptop2  23635  qtopid  23641  trfg  23827  flfneii  23928  fclsbas  23957  isfcf  23970  restutop  24174  restutopopn  24175  isucn2  24215  cfiluexsm  24226  cfilufg  24229  blgt0  24336  xblss2ps  24338  xblss2  24339  mopni  24429  metrest  24461  metustbl  24503  restmetu  24507  cfilss  25220  caun0  25231  cmetcaulem  25238  cfilresi  25245  cmetcusp  25304  cnlimci  25840  dvcl  25850  dvcnp  25870  dvcnp2  25871  dvcnp2OLD  25872  dvnadd  25881  dvfsumrlimge0  25987  dvfsumrlim  25988  dvfsumrlim2  25989  fta1g  26125  plyeq0lem  26165  vieta1lem1  26268  vieta1lem2  26269  fsumharmonic  26972  dvdsflf1o  27147  dvdsflsumcom  27148  fsumvma  27174  vmadivsumb  27444  dchrisum0lem1a  27447  dchrisumlema  27449  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0fno1  27472  dchrisum0lem1b  27476  mulog2sumlem2  27496  vmalogdivsum2  27499  2vmadivsumlem  27501  selberglem2  27507  selbergb  27510  selberg2b  27513  selberg3lem1  27518  selberg4lem1  27521  pntpbnd1  27547  pntibndlem3  27553  pntlem3  27570  ssltleft  27826  ssltright  27827  cofcutr  27875  oppnid  28671  sspba  30654  sspg  30655  ssps  30657  sspn  30663  nmblore  30713  phpar  30751  ocorth  31218  elnlfn2  31856  foresf1o  32431  fnpreimac  32595  fpwrelmap  32656  elrgspnsubrunlem2  33189  kerunit  33287  0nellinds  33331  linds2eq  33342  dvdsruasso  33346  unitpidl1  33385  rhmpreimaprmidl  33412  mxidlirredi  33432  rprmdvds  33480  rprmnz  33481  1arithufdlem3  33507  ply1unit  33534  ply1degltlss  33552  exsslsb  33582  ply1degltdimlem  33608  lindsunlem  33610  dimkerim  33613  irngss  33674  0ringirng  33676  irngnminplynz  33692  algextdeglem8  33704  reff  33816  cnre2csqlem  33887  fmcncfil  33908  elzrhunit  33954  qqhval2lem  33958  baselsiga  34092  signsply0  34529  cvmliftmolem1  35249  mclsppslem  35551  mclspps  35552  fnetr  36315  relowlssretop  37327  mbfresfi  37636  itg2addnclem  37641  itg2addnclem2  37642  sstotbnd2  37744  rngoiso1o  37949  pridl  38007  lfli  39025  lkrf0  39057  cvrne  39245  atcvr0  39252  psubspi  39712  psubcli2N  39904  lhp1cvr  39964  lautle  40049  diadmleN  41003  sn-eluzp1l  42304  cvgdvgrat  44285  radcnvrat  44286  projf1o  45169  islptre  45596  islpcn  45616  icccncfext  45864  fdivmptf  48469  refdivmptf  48470  rege1logbrege0  48486  nelsubc2  48984  termcterm2  49347