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  9591  fseqenlem2  9926  axdc3lem2  10352  fpwwe2lem11  10542  rlimsqzlem  15566  ramub1lem2  16949  invfun  17681  pltne  18248  cntzi  19251  odmulg  19478  subgslw  19538  frgpnabllem1  19795  cyggeninv  19805  ablfaclem3  20011  lsslmod  20903  rhmpreimaidl  21224  psgnevpm  21536  pjff  21659  pjf2  21661  pjcss  21663  ocvpj  21664  evlslem3  22025  mhpdeg  22070  scmatscmid  22431  fvmptnn04ifc  22777  fvmptnn04ifd  22778  tgcl  22894  cldopn  22956  cncnp  23205  1stcelcls  23386  lly1stc  23421  refssex  23436  qtoptop2  23624  qtopid  23630  trfg  23816  flfneii  23917  fclsbas  23946  isfcf  23959  restutop  24162  restutopopn  24163  isucn2  24203  cfiluexsm  24214  cfilufg  24217  blgt0  24324  xblss2ps  24326  xblss2  24327  mopni  24417  metrest  24449  metustbl  24491  restmetu  24495  cfilss  25207  caun0  25218  cmetcaulem  25225  cfilresi  25232  cmetcusp  25291  cnlimci  25827  dvcl  25837  dvcnp  25857  dvcnp2  25858  dvcnp2OLD  25859  dvnadd  25868  dvfsumrlimge0  25974  dvfsumrlim  25975  dvfsumrlim2  25976  fta1g  26112  plyeq0lem  26152  vieta1lem1  26255  vieta1lem2  26256  fsumharmonic  26959  dvdsflf1o  27134  dvdsflsumcom  27135  fsumvma  27161  vmadivsumb  27431  dchrisum0lem1a  27434  dchrisumlema  27436  dchrisumlem3  27439  dchrmusum2  27442  dchrvmasumlem2  27446  dchrvmasumiflem1  27449  dchrisum0fno1  27459  dchrisum0lem1b  27463  mulog2sumlem2  27483  vmalogdivsum2  27486  2vmadivsumlem  27488  selberglem2  27494  selbergb  27497  selberg2b  27500  selberg3lem1  27505  selberg4lem1  27508  pntpbnd1  27534  pntibndlem3  27540  pntlem3  27557  ssltleft  27825  ssltright  27826  cofcutr  27878  oppnid  28734  sspba  30718  sspg  30719  ssps  30721  sspn  30727  nmblore  30777  phpar  30815  ocorth  31282  elnlfn2  31920  foresf1o  32495  fnpreimac  32664  fpwrelmap  32727  elrgspnsubrunlem2  33226  kerunit  33301  0nellinds  33346  linds2eq  33357  dvdsruasso  33361  unitpidl1  33400  rhmpreimaprmidl  33427  mxidlirredi  33447  rprmdvds  33495  rprmnz  33496  1arithufdlem3  33522  ply1unit  33549  ply1degltlss  33568  exsslsb  33620  ply1degltdimlem  33646  lindsunlem  33648  dimkerim  33651  irngss  33711  0ringirng  33713  irngnminplynz  33736  algextdeglem8  33748  reff  33863  cnre2csqlem  33934  fmcncfil  33955  elzrhunit  34001  qqhval2lem  34005  baselsiga  34139  signsply0  34575  cvmliftmolem1  35336  mclsppslem  35638  mclspps  35639  fnetr  36406  relowlssretop  37418  mbfresfi  37716  itg2addnclem  37721  itg2addnclem2  37722  sstotbnd2  37824  rngoiso1o  38029  pridl  38087  lfli  39170  lkrf0  39202  cvrne  39390  atcvr0  39397  psubspi  39856  psubcli2N  40048  lhp1cvr  40108  lautle  40193  diadmleN  41147  sn-eluzp1l  42416  cvgdvgrat  44420  radcnvrat  44421  projf1o  45308  islptre  45733  islpcn  45751  icccncfext  45999  fdivmptf  48656  refdivmptf  48657  rege1logbrege0  48673  nelsubc2  49184  termcterm2  49629