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  9644  fseqenlem2  9978  axdc3lem2  10404  fpwwe2lem11  10594  rlimsqzlem  15615  ramub1lem2  16998  invfun  17726  pltne  18293  cntzi  19261  odmulg  19486  subgslw  19546  frgpnabllem1  19803  cyggeninv  19813  ablfaclem3  20019  lsslmod  20866  rhmpreimaidl  21187  psgnevpm  21498  pjff  21621  pjf2  21623  pjcss  21625  ocvpj  21626  evlslem3  21987  mhpdeg  22032  scmatscmid  22393  fvmptnn04ifc  22739  fvmptnn04ifd  22740  tgcl  22856  cldopn  22918  cncnp  23167  1stcelcls  23348  lly1stc  23383  refssex  23398  qtoptop2  23586  qtopid  23592  trfg  23778  flfneii  23879  fclsbas  23908  isfcf  23921  restutop  24125  restutopopn  24126  isucn2  24166  cfiluexsm  24177  cfilufg  24180  blgt0  24287  xblss2ps  24289  xblss2  24290  mopni  24380  metrest  24412  metustbl  24454  restmetu  24458  cfilss  25170  caun0  25181  cmetcaulem  25188  cfilresi  25195  cmetcusp  25254  cnlimci  25790  dvcl  25800  dvcnp  25820  dvcnp2  25821  dvcnp2OLD  25822  dvnadd  25831  dvfsumrlimge0  25937  dvfsumrlim  25938  dvfsumrlim2  25939  fta1g  26075  plyeq0lem  26115  vieta1lem1  26218  vieta1lem2  26219  fsumharmonic  26922  dvdsflf1o  27097  dvdsflsumcom  27098  fsumvma  27124  vmadivsumb  27394  dchrisum0lem1a  27397  dchrisumlema  27399  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0fno1  27422  dchrisum0lem1b  27426  mulog2sumlem2  27446  vmalogdivsum2  27449  2vmadivsumlem  27451  selberglem2  27457  selbergb  27460  selberg2b  27463  selberg3lem1  27468  selberg4lem1  27471  pntpbnd1  27497  pntibndlem3  27503  pntlem3  27520  ssltleft  27782  ssltright  27783  cofcutr  27832  oppnid  28673  sspba  30656  sspg  30657  ssps  30659  sspn  30665  nmblore  30715  phpar  30753  ocorth  31220  elnlfn2  31858  foresf1o  32433  fnpreimac  32595  fpwrelmap  32656  elrgspnsubrunlem2  33199  kerunit  33297  0nellinds  33341  linds2eq  33352  dvdsruasso  33356  unitpidl1  33395  rhmpreimaprmidl  33422  mxidlirredi  33442  rprmdvds  33490  rprmnz  33491  1arithufdlem3  33517  ply1unit  33544  ply1degltlss  33562  exsslsb  33592  ply1degltdimlem  33618  lindsunlem  33620  dimkerim  33623  irngss  33682  0ringirng  33684  irngnminplynz  33702  algextdeglem8  33714  reff  33829  cnre2csqlem  33900  fmcncfil  33921  elzrhunit  33967  qqhval2lem  33971  baselsiga  34105  signsply0  34542  cvmliftmolem1  35268  mclsppslem  35570  mclspps  35571  fnetr  36339  relowlssretop  37351  mbfresfi  37660  itg2addnclem  37665  itg2addnclem2  37666  sstotbnd2  37768  rngoiso1o  37973  pridl  38031  lfli  39054  lkrf0  39086  cvrne  39274  atcvr0  39281  psubspi  39741  psubcli2N  39933  lhp1cvr  39993  lautle  40078  diadmleN  41032  sn-eluzp1l  42296  cvgdvgrat  44302  radcnvrat  44303  projf1o  45191  islptre  45617  islpcn  45637  icccncfext  45885  fdivmptf  48530  refdivmptf  48531  rege1logbrege0  48547  nelsubc2  49058  termcterm2  49503