Theorem anbi2d 464

Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32d 450	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi2  467  anbi1cd  468  anbi12d  473  bi2anan9  606  dn1dc  962  xorbi2d  1391  dfbi3dc  1408  xordidc  1410  eleq2w  2258  eleq2  2260  ceqsex2  2804  ceqsex6v  2808  vtocl2gaf  2831  ceqsrex2v  2896  mob2  2944  eqreu  2956  nelrdva  2971  dfss4st  3397  undif4  3514  r19.27m  3547  ifbi  3582  preq12bg  3804  opeq2  3810  ralunsn  3828  intab  3904  disjiun  4029  brimralrspcev  4093  opabbid  4099  opthg  4272  pocl  4339  ordelord  4417  ordtriexmid  4558  ontr2exmid  4562  onsucsssucexmid  4564  tfisi  4624  xpeq2  4679  rabxp  4701  vtoclr  4712  opeliunxp  4719  posng  4736  opbrop  4743  rexiunxp  4809  elrnmpt1  4918  dfres2  4999  brcodir  5058  poltletr  5071  xp11m  5109  elxp4  5158  elxp5  5159  dffun4f  5275  fununi  5327  fneq2  5348  fnun  5367  feq3  5395  foeq3  5481  funfveu  5574  funbrfv  5602  ssimaexg  5626  fvopab3g  5637  fvopab3ig  5638  fvelrn  5696  fmptco  5731  fsn2  5739  elunirn  5816  isoeq2  5852  isoeq3  5853  isocnv2  5862  isoini  5868  isopolem  5872  f1oiso  5876  f1oiso2  5877  oprabbid  5979  cbvoprab3  6002  mpomptx  6017  mpofun  6028  ov  6046  ovi3  6064  ov6g  6065  ovg  6066  caoftrn  6172  uchoice  6204  f1o2ndf1  6295  xporderlem  6298  f1od2  6302  brtpos2  6318  brtposg  6321  dftpos4  6330  recseq  6373  tfrlem3-2d  6379  tfrlemi1  6399  tfrexlem  6401  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcl  6431  freceq1  6459  freceq2  6460  frecsuc  6474  nnaordex  6595  brecop  6693  eroveu  6694  erovlem  6695  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3qlem2  6706  th3q  6708  elpmg  6732  ixpsnval  6769  ixpsnf1o  6804  domeng  6820  dom2lem  6840  xpcomco  6894  xpassen  6898  xpdom2  6899  xpf1o  6914  phplem3g  6926  ssfiexmid  6946  domfiexmid  6948  findcard2  6959  findcard2s  6960  findcard2d  6961  findcard2sd  6962  diffifi  6964  fiintim  7001  opabfi  7008  fidcenumlemrk  7029  fidcenumlemr  7030  supeq2  7064  nninfninc  7198  nnnninfeq2  7204  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  isacnm  7288  acfun  7292  2omotaplemap  7342  2omotaplemst  7343  exmidapne  7345  ccfunen  7349  recexnq  7476  recmulnqg  7477  ltsonq  7484  enq0sym  7518  enq0ref  7519  enq0tr  7520  enq0breq  7522  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  mulnnnq0  7536  elinp  7560  prdisj  7578  prarloclem3  7583  prarloc  7589  distrlem5prl  7672  distrlem5pru  7673  ltexprlemell  7684  ltexprlemelu  7685  recexprlemm  7710  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  lttrsr  7848  recexgt0sr  7859  mulgt0sr  7864  ltresr  7925  axprecex  7966  axpre-lttrn  7970  axpre-mulgt0  7973  eqlelt  8132  lesub0  8525  apreap  8633  apreim  8649  aprcl  8692  aptap  8696  zltlen  9423  prime  9444  fzind  9460  qltlen  9733  xltnegi  9929  ixxval  9990  fzval  10104  fzdifsuc  10175  elfzm11  10185  elfzo  10243  zsupcllemex  10339  exbtwnzlemshrink  10357  rebtwn2zlemshrink  10362  facwordi  10851  zfz1iso  10952  shftfvalg  11002  shftfibg  11004  shftfval  11005  shftfib  11007  shftfn  11008  2shfti  11015  cau3lem  11298  caubnd2  11301  xrmaxiflemcom  11433  clim  11465  clim2  11467  climi  11471  climcn2  11493  addcn2  11494  subcn2  11495  mulcn2  11496  summodclem2a  11565  summodc  11567  fsum3  11571  fsumsplitf  11592  prodfdivap  11731  ntrivcvgap0  11733  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  fproddivapf  11815  fprodsplitf  11816  fprodsplit1f  11818  sinbnd  11936  cosbnd  11937  divalgb  12109  ndvdssub  12114  gcdval  12153  gcdneg  12176  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  dfgcd2  12208  gcdass  12209  algcvgblem  12244  lcmval  12258  lcmneg  12269  lcmgcdlem  12272  lcmass  12280  qredeq  12291  prmind2  12315  euclemma  12341  pw2dvdslemn  12360  qnumval  12380  qdenval  12381  pceu  12491  pczpre  12493  pcdiv  12498  prmpwdvds  12551  prdsex  12973  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  gsum0g  13100  mnd1  13159  grp1  13310  qusgrp2  13321  nmznsg  13421  releqgg  13428  eqgex  13429  iscmnd  13506  issrg  13599  iscrng2  13649  qusring2  13700  opprunitd  13744  crngunit  13745  dfrhm2  13788  rhmopp  13810  issubrng  13833  resrhm2b  13883  islmod  13925  lsssetm  13990  lsspropdg  14065  ixpsnbasval  14100  basis2  14392  eltg2  14397  isnei  14488  isneip  14490  restbasg  14512  iscnp  14543  iscnp3  14547  tgcn  14552  icnpimaex  14555  lmbrf  14559  cncnp  14574  cnptoprest2  14584  txbas  14602  txcnp  14615  imasnopn  14643  ispsmet  14667  ismet  14688  isxmet  14689  ismet2  14698  blres  14778  metcnp3  14855  txmetcnp  14862  mulcncf  14952  ellimc3apf  15004  limcdifap  15006  limcmpted  15007  limccnp2lem  15020  dvmptfsum  15069  elply2  15079  sincosq3sgn  15172  lgsquadlem1  15426  2sqlem8  15472  2sqlem9  15473  subctctexmid  15755  nnnninfex  15777