Theorem simplbda 505

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 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 501	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cantnflem3  9673  fseqenlem2  10031  axdc3lem2  10456  fpwwe2lem11  10653  rlimsqzlem  15738  ramub1lem2  17123  invfun  17857  pltne  18424  cntzi  19460  odmulg  19687  subgslw  19747  frgpnabllem1  20004  cyggeninv  20014  ablfaclem3  20220  lsslmod  21148  rhmpreimaidl  21483  rhmpreimaprmidl  21546  psgnevpm  21806  pjff  21929  pjf2  21931  pjcss  21933  ocvpj  21934  evlslem3  22300  mhpdeg  22377  scmatscmid  22732  fvmptnn04ifc  23081  fvmptnn04ifd  23082  tgcl  23198  cldopn  23260  cncnp  23509  1stcelcls  23691  lly1stc  23726  refssex  23741  qtoptop2  23929  qtopid  23935  trfg  24121  flfneii  24222  fclsbas  24251  isfcf  24264  restutop  24467  restutopopn  24468  isucn2  24508  cfiluexsm  24519  cfilufg  24522  blgt0  24629  xblss2ps  24631  xblss2  24632  mopni  24722  metrest  24754  metustbl  24796  restmetu  24800  cfilss  25502  caun0  25513  cmetcaulem  25520  cfilresi  25527  cmetcusp  25586  cnlimci  26121  dvcl  26131  dvcnp  26151  dvcnp2  26152  dvnadd  26161  dvfsumrlimge0  26262  dvfsumrlim  26263  dvfsumrlim2  26264  fta1g  26400  plyeq0lem  26440  vieta1lem1  26544  vieta1lem2  26545  fsumharmonic  27249  dvdsflf1o  27424  dvdsflsumcom  27425  fsumvma  27450  vmadivsumb  27720  dchrisum0lem1a  27723  dchrisumlema  27725  dchrisumlem3  27728  dchrmusum2  27731  dchrvmasumlem2  27735  dchrvmasumiflem1  27738  dchrisum0fno1  27748  dchrisum0lem1b  27752  mulog2sumlem2  27772  vmalogdivsum2  27775  2vmadivsumlem  27777  selberglem2  27783  selbergb  27786  selberg2b  27789  selberg3lem1  27794  selberg4lem1  27797  pntpbnd1  27823  pntibndlem3  27829  pntlem3  27846  sltsleft  28126  sltsright  28127  cofcutr  28190  oppnid  29102  prlnghpg  29304  sspba  31209  sspg  31210  ssps  31212  sspn  31218  nmblore  31268  phpar  31306  ocorth  31773  elnlfn2  32411  foresf1o  32980  fnpreimac  33145  fpwrelmap  33206  elrgspnsubrunlem2  33690  kerunit  33767  0nellinds  33807  linds2eq  33816  dvdsruasso  33820  unitpidl1  33854  mxidlirredi  33876  dflringlem2  33907  rprmdvds  33931  rprmnz  33932  1arithufdlem3  33958  ply1unit  33987  ply1degltlss  34008  selvply1rhmlema  34030  selvply1rhmlem1  34032  esplyfvaln  34086  exsslsb  34109  ply1degltdimlem  34134  lindsunlem  34136  dimkerim  34139  irngss  34199  0ringirng  34201  irngnminplynz  34224  algextdeglem8  34236  reff  34351  cnre2csqlem  34422  fmcncfil  34443  elzrhunit  34489  qqhval2lem  34493  baselsiga  34627  signsply0  35061  cvmliftmolem1  35862  mclsppslem  36164  mclspps  36165  fnetr  36972  relowlssretop  38119  mbfresfi  38417  itg2addnclem  38422  itg2addnclem2  38423  sstotbnd2  38526  rngoiso1o  38731  pridl  38789  lfli  39936  lkrf0  39968  cvrne  40156  atcvr0  40163  psubspi  40622  psubcli2N  40814  lhp1cvr  40874  lautle  40959  diadmleN  41913  sn-eluzp1l  43185  cvgdvgrat  45139  radcnvrat  45140  projf1o  46030  islptre  46451  islpcn  46469  icccncfext  46717  fdivmptf  49473  refdivmptf  49474  rege1logbrege0  49490  nelsubc2  49997  termcterm2  50442