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  9651  fseqenlem2  9985  axdc3lem2  10411  fpwwe2lem11  10601  rlimsqzlem  15622  ramub1lem2  17005  invfun  17733  pltne  18300  cntzi  19268  odmulg  19493  subgslw  19553  frgpnabllem1  19810  cyggeninv  19820  ablfaclem3  20026  lsslmod  20873  rhmpreimaidl  21194  psgnevpm  21505  pjff  21628  pjf2  21630  pjcss  21632  ocvpj  21633  evlslem3  21994  mhpdeg  22039  scmatscmid  22400  fvmptnn04ifc  22746  fvmptnn04ifd  22747  tgcl  22863  cldopn  22925  cncnp  23174  1stcelcls  23355  lly1stc  23390  refssex  23405  qtoptop2  23593  qtopid  23599  trfg  23785  flfneii  23886  fclsbas  23915  isfcf  23928  restutop  24132  restutopopn  24133  isucn2  24173  cfiluexsm  24184  cfilufg  24187  blgt0  24294  xblss2ps  24296  xblss2  24297  mopni  24387  metrest  24419  metustbl  24461  restmetu  24465  cfilss  25177  caun0  25188  cmetcaulem  25195  cfilresi  25202  cmetcusp  25261  cnlimci  25797  dvcl  25807  dvcnp  25827  dvcnp2  25828  dvcnp2OLD  25829  dvnadd  25838  dvfsumrlimge0  25944  dvfsumrlim  25945  dvfsumrlim2  25946  fta1g  26082  plyeq0lem  26122  vieta1lem1  26225  vieta1lem2  26226  fsumharmonic  26929  dvdsflf1o  27104  dvdsflsumcom  27105  fsumvma  27131  vmadivsumb  27401  dchrisum0lem1a  27404  dchrisumlema  27406  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0fno1  27429  dchrisum0lem1b  27433  mulog2sumlem2  27453  vmalogdivsum2  27456  2vmadivsumlem  27458  selberglem2  27464  selbergb  27467  selberg2b  27470  selberg3lem1  27475  selberg4lem1  27478  pntpbnd1  27504  pntibndlem3  27510  pntlem3  27527  ssltleft  27789  ssltright  27790  cofcutr  27839  oppnid  28680  sspba  30663  sspg  30664  ssps  30666  sspn  30672  nmblore  30722  phpar  30760  ocorth  31227  elnlfn2  31865  foresf1o  32440  fnpreimac  32602  fpwrelmap  32663  elrgspnsubrunlem2  33206  kerunit  33304  0nellinds  33348  linds2eq  33359  dvdsruasso  33363  unitpidl1  33402  rhmpreimaprmidl  33429  mxidlirredi  33449  rprmdvds  33497  rprmnz  33498  1arithufdlem3  33524  ply1unit  33551  ply1degltlss  33569  exsslsb  33599  ply1degltdimlem  33625  lindsunlem  33627  dimkerim  33630  irngss  33689  0ringirng  33691  irngnminplynz  33709  algextdeglem8  33721  reff  33836  cnre2csqlem  33907  fmcncfil  33928  elzrhunit  33974  qqhval2lem  33978  baselsiga  34112  signsply0  34549  cvmliftmolem1  35275  mclsppslem  35577  mclspps  35578  fnetr  36346  relowlssretop  37358  mbfresfi  37667  itg2addnclem  37672  itg2addnclem2  37673  sstotbnd2  37775  rngoiso1o  37980  pridl  38038  lfli  39061  lkrf0  39093  cvrne  39281  atcvr0  39288  psubspi  39748  psubcli2N  39940  lhp1cvr  40000  lautle  40085  diadmleN  41039  sn-eluzp1l  42303  cvgdvgrat  44309  radcnvrat  44310  projf1o  45198  islptre  45624  islpcn  45644  icccncfext  45892  fdivmptf  48534  refdivmptf  48535  rege1logbrege0  48551  nelsubc2  49062  termcterm2  49507