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  610  dn1dc  968  dfifp3dc  990  ifpdfbidc  993  xorbi2d  1424  dfbi3dc  1441  xordidc  1443  eleq2w  2293  eleq2  2295  ceqsex2  2844  ceqsex6v  2848  vtocl2gaf  2871  ceqsrex2v  2938  mob2  2986  eqreu  2998  nelrdva  3013  dfss4st  3440  undif4  3557  r19.27m  3590  ifbi  3626  preq12bg  3856  opeq2  3863  ralunsn  3881  intab  3957  disjiun  4083  brimralrspcev  4148  opabbid  4154  opthg  4330  pocl  4400  ordelord  4478  ordtriexmid  4619  ontr2exmid  4623  onsucsssucexmid  4625  tfisi  4685  xpeq2  4740  rabxp  4763  vtoclr  4774  opeliunxp  4781  posng  4798  opbrop  4805  rexiunxp  4872  elrnmpt1  4983  dfres2  5065  brcodir  5124  poltletr  5137  xp11m  5175  elxp4  5224  elxp5  5225  dffun4f  5342  fununi  5398  fneq2  5419  fnun  5438  feq3  5467  foeq3  5557  funfveu  5652  funbrfv  5682  ssimaexg  5708  fvopab3g  5719  fvopab3ig  5720  fvelrn  5778  fmptco  5813  fsn2  5821  elunirn  5906  isoeq2  5942  isoeq3  5943  isocnv2  5952  isoini  5958  isopolem  5962  f1oiso  5966  f1oiso2  5967  oprabbid  6073  cbvoprab3  6096  mpomptx  6111  mpofun  6122  ov  6140  ovi3  6158  ov6g  6159  ovg  6160  caoftrn  6267  uchoice  6299  f1o2ndf1  6392  xporderlem  6395  f1od2  6399  brtpos2  6416  brtposg  6419  dftpos4  6428  recseq  6471  tfrlem3-2d  6477  tfrlemi1  6497  tfrexlem  6499  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcl  6529  freceq1  6557  freceq2  6558  frecsuc  6572  nnaordex  6695  brecop  6793  eroveu  6794  erovlem  6795  ecopovtrn  6800  ecopovtrng  6803  th3qlem1  6805  th3qlem2  6806  th3q  6808  elpmg  6832  ixpsnval  6869  ixpsnf1o  6904  domeng  6922  dom2lem  6944  modom  6993  xpcomco  7009  xpassen  7013  xpdom2  7014  xpf1o  7029  phplem3g  7041  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  findcard2  7077  findcard2s  7078  findcard2d  7079  findcard2sd  7080  diffifi  7082  fiintim  7122  opabfi  7131  fidcenumlemrk  7152  fidcenumlemr  7153  supeq2  7187  nninfninc  7321  nnnninfeq2  7327  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  isacnm  7417  acfun  7421  2omotaplemap  7475  2omotaplemst  7476  exmidapne  7478  ccfunen  7482  recexnq  7609  recmulnqg  7610  ltsonq  7617  enq0sym  7651  enq0ref  7652  enq0tr  7653  enq0breq  7655  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  elinp  7693  prdisj  7711  prarloclem3  7716  prarloc  7722  distrlem5prl  7805  distrlem5pru  7806  ltexprlemell  7817  ltexprlemelu  7818  recexprlemm  7843  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  lttrsr  7981  recexgt0sr  7992  mulgt0sr  7997  ltresr  8058  axprecex  8099  axpre-lttrn  8103  axpre-mulgt0  8106  eqlelt  8265  lesub0  8658  apreap  8766  apreim  8782  aprcl  8825  aptap  8829  zltlen  9557  prime  9578  fzind  9594  qltlen  9873  xltnegi  10069  ixxval  10130  fzval  10244  fzdifsuc  10315  elfzm11  10325  elfzo  10383  zsupcllemex  10489  exbtwnzlemshrink  10507  rebtwn2zlemshrink  10512  facwordi  11001  zfz1iso  11104  pfxsuff1eqwrdeq  11279  wrd2ind  11303  shftfvalg  11378  shftfibg  11380  shftfval  11381  shftfib  11383  shftfn  11384  2shfti  11391  cau3lem  11674  caubnd2  11677  xrmaxiflemcom  11809  clim  11841  clim2  11843  climi  11847  climcn2  11869  addcn2  11870  subcn2  11871  mulcn2  11872  summodclem2a  11941  summodc  11943  fsum3  11947  fsumsplitf  11968  prodfdivap  12107  ntrivcvgap0  12109  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  sinbnd  12312  cosbnd  12313  divalgb  12485  ndvdssub  12490  gcdval  12529  gcdneg  12552  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  dfgcd2  12584  gcdass  12585  algcvgblem  12620  lcmval  12634  lcmneg  12645  lcmgcdlem  12648  lcmass  12656  qredeq  12667  prmind2  12691  euclemma  12717  pw2dvdslemn  12736  qnumval  12756  qdenval  12757  pceu  12867  pczpre  12869  pcdiv  12874  prmpwdvds  12927  prdsex  13351  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  gsum0g  13478  mnd1  13537  grp1  13688  qusgrp2  13699  nmznsg  13799  releqgg  13806  eqgex  13807  iscmnd  13884  issrg  13977  iscrng2  14027  qusring2  14078  opprunitd  14123  crngunit  14124  dfrhm2  14167  rhmopp  14189  issubrng  14212  resrhm2b  14262  islmod  14304  lsssetm  14369  lsspropdg  14444  ixpsnbasval  14479  basis2  14771  eltg2  14776  isnei  14867  isneip  14869  restbasg  14891  iscnp  14922  iscnp3  14926  tgcn  14931  icnpimaex  14934  lmbrf  14938  cncnp  14953  cnptoprest2  14963  txbas  14981  txcnp  14994  imasnopn  15022  ispsmet  15046  ismet  15067  isxmet  15068  ismet2  15077  blres  15157  metcnp3  15234  txmetcnp  15241  mulcncf  15331  ellimc3apf  15383  limcdifap  15385  limcmpted  15386  limccnp2lem  15399  dvmptfsum  15448  elply2  15458  sincosq3sgn  15551  lgsquadlem1  15805  2sqlem8  15851  2sqlem9  15852  eupthres  16307  subctctexmid  16601  nnnninfex  16624  gfsumval  16680