Theorem simplbda 504

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simplbda	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 500	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  cantnflem3  9659  fseqenlem2  10008  axdc3lem2  10434  fpwwe2lem11  10625  rlimsqzlem  15700  ramub1lem2  17086  invfun  17820  pltne  18387  cntzi  19398  odmulg  19625  subgslw  19685  frgpnabllem1  19942  cyggeninv  19952  ablfaclem3  20158  lsslmod  21060  rhmpreimaidl  21395  rhmpreimaprmidl  21458  psgnevpm  21718  pjff  21841  pjf2  21843  pjcss  21845  ocvpj  21846  evlslem3  22210  mhpdeg  22287  scmatscmid  22642  fvmptnn04ifc  22988  fvmptnn04ifd  22989  tgcl  23105  cldopn  23167  cncnp  23416  1stcelcls  23597  lly1stc  23632  refssex  23647  qtoptop2  23835  qtopid  23841  trfg  24027  flfneii  24128  fclsbas  24157  isfcf  24170  restutop  24373  restutopopn  24374  isucn2  24414  cfiluexsm  24425  cfilufg  24428  blgt0  24535  xblss2ps  24537  xblss2  24538  mopni  24628  metrest  24660  metustbl  24702  restmetu  24706  cfilss  25408  caun0  25419  cmetcaulem  25426  cfilresi  25433  cmetcusp  25492  cnlimci  26027  dvcl  26037  dvcnp  26057  dvcnp2  26058  dvnadd  26067  dvfsumrlimge0  26168  dvfsumrlim  26169  dvfsumrlim2  26170  fta1g  26306  plyeq0lem  26346  vieta1lem1  26450  vieta1lem2  26451  fsumharmonic  27152  dvdsflf1o  27327  dvdsflsumcom  27328  fsumvma  27353  vmadivsumb  27623  dchrisum0lem1a  27626  dchrisumlema  27628  dchrisumlem3  27631  dchrmusum2  27634  dchrvmasumlem2  27638  dchrvmasumiflem1  27641  dchrisum0fno1  27651  dchrisum0lem1b  27655  mulog2sumlem2  27675  vmalogdivsum2  27678  2vmadivsumlem  27680  selberglem2  27686  selbergb  27689  selberg2b  27692  selberg3lem1  27697  selberg4lem1  27700  pntpbnd1  27726  pntibndlem3  27732  pntlem3  27749  sltsleft  28029  sltsright  28030  cofcutr  28093  oppnid  29002  prlnghpg  29169  sspba  31045  sspg  31046  ssps  31048  sspn  31054  nmblore  31104  phpar  31142  ocorth  31609  elnlfn2  32247  foresf1o  32816  fnpreimac  32981  fpwrelmap  33044  elrgspnsubrunlem2  33534  kerunit  33611  0nellinds  33651  linds2eq  33660  dvdsruasso  33664  unitpidl1  33698  mxidlirredi  33720  dflringlem2  33751  rprmdvds  33775  rprmnz  33776  1arithufdlem3  33802  ply1unit  33831  ply1degltlss  33852  selvply1rhmlema  33874  selvply1rhmlem1  33876  esplyfvaln  33930  exsslsb  33953  ply1degltdimlem  33978  lindsunlem  33980  dimkerim  33983  irngss  34043  0ringirng  34045  irngnminplynz  34068  algextdeglem8  34080  reff  34195  cnre2csqlem  34266  fmcncfil  34287  elzrhunit  34333  qqhval2lem  34337  baselsiga  34471  signsply0  34904  cvmliftmolem1  35739  mclsppslem  36041  mclspps  36042  fnetr  36828  relowlssretop  37975  mbfresfi  38283  itg2addnclem  38288  itg2addnclem2  38289  sstotbnd2  38391  rngoiso1o  38596  pridl  38654  lfli  39803  lkrf0  39835  cvrne  40023  atcvr0  40030  psubspi  40489  psubcli2N  40681  lhp1cvr  40741  lautle  40826  diadmleN  41780  sn-eluzp1l  43037  cvgdvgrat  44993  radcnvrat  44994  projf1o  45884  islptre  46305  islpcn  46323  icccncfext  46571  fdivmptf  49288  refdivmptf  49289  rege1logbrege0  49305  nelsubc2  49814  termcterm2  50259