Theorem simplbda 499

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 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  9612  fseqenlem2  9947  axdc3lem2  10373  fpwwe2lem11  10564  rlimsqzlem  15584  ramub1lem2  16967  invfun  17700  pltne  18267  cntzi  19270  odmulg  19497  subgslw  19557  frgpnabllem1  19814  cyggeninv  19824  ablfaclem3  20030  lsslmod  20923  rhmpreimaidl  21244  psgnevpm  21556  pjff  21679  pjf2  21681  pjcss  21683  ocvpj  21684  evlslem3  22047  mhpdeg  22100  scmatscmid  22462  fvmptnn04ifc  22808  fvmptnn04ifd  22809  tgcl  22925  cldopn  22987  cncnp  23236  1stcelcls  23417  lly1stc  23452  refssex  23467  qtoptop2  23655  qtopid  23661  trfg  23847  flfneii  23948  fclsbas  23977  isfcf  23990  restutop  24193  restutopopn  24194  isucn2  24234  cfiluexsm  24245  cfilufg  24248  blgt0  24355  xblss2ps  24357  xblss2  24358  mopni  24448  metrest  24480  metustbl  24522  restmetu  24526  cfilss  25238  caun0  25249  cmetcaulem  25256  cfilresi  25263  cmetcusp  25322  cnlimci  25858  dvcl  25868  dvcnp  25888  dvcnp2  25889  dvcnp2OLD  25890  dvnadd  25899  dvfsumrlimge0  26005  dvfsumrlim  26006  dvfsumrlim2  26007  fta1g  26143  plyeq0lem  26183  vieta1lem1  26286  vieta1lem2  26287  fsumharmonic  26990  dvdsflf1o  27165  dvdsflsumcom  27166  fsumvma  27192  vmadivsumb  27462  dchrisum0lem1a  27465  dchrisumlema  27467  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0fno1  27490  dchrisum0lem1b  27494  mulog2sumlem2  27514  vmalogdivsum2  27517  2vmadivsumlem  27519  selberglem2  27525  selbergb  27528  selberg2b  27531  selberg3lem1  27536  selberg4lem1  27539  pntpbnd1  27565  pntibndlem3  27571  pntlem3  27588  sltsleft  27868  sltsright  27869  cofcutr  27932  oppnid  28830  sspba  30814  sspg  30815  ssps  30817  sspn  30823  nmblore  30873  phpar  30911  ocorth  31378  elnlfn2  32016  foresf1o  32590  fnpreimac  32759  fpwrelmap  32822  elrgspnsubrunlem2  33341  kerunit  33417  0nellinds  33462  linds2eq  33473  dvdsruasso  33477  unitpidl1  33516  rhmpreimaprmidl  33543  mxidlirredi  33563  rprmdvds  33611  rprmnz  33612  1arithufdlem3  33638  ply1unit  33667  ply1degltlss  33688  esplyfvaln  33750  exsslsb  33773  ply1degltdimlem  33799  lindsunlem  33801  dimkerim  33804  irngss  33864  0ringirng  33866  irngnminplynz  33889  algextdeglem8  33901  reff  34016  cnre2csqlem  34087  fmcncfil  34108  elzrhunit  34154  qqhval2lem  34158  baselsiga  34292  signsply0  34728  cvmliftmolem1  35494  mclsppslem  35796  mclspps  35797  fnetr  36564  relowlssretop  37607  mbfresfi  37906  itg2addnclem  37911  itg2addnclem2  37912  sstotbnd2  38014  rngoiso1o  38219  pridl  38277  lfli  39426  lkrf0  39458  cvrne  39646  atcvr0  39653  psubspi  40112  psubcli2N  40304  lhp1cvr  40364  lautle  40449  diadmleN  41403  sn-eluzp1l  42667  cvgdvgrat  44658  radcnvrat  44659  projf1o  45544  islptre  45968  islpcn  45986  icccncfext  46234  fdivmptf  48890  refdivmptf  48891  rege1logbrege0  48907  nelsubc2  49417  termcterm2  49862