Theorem anbi2i 629

Description: Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi2i	⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32i 579	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi1ci  632  anbi12i  634  bianass  648  an42  663  anandir  683  dfbi3  1055  dn1  1063  dfifp3  1071  ifpdfbi  1076  4anpull2  1368  an3andi  1490  an33rean  1491  anxordi  1533  cadcoma  1619  nic-mpALT  1679  nic-axALT  1681  3exdistr  1967  4exdistr  1968  19.27v  2002  19.27  2239  19.41  2247  2sb5  2289  dfsb7  2290  dfeumo  2540  mo4f  2571  eu3v  2574  eu6  2578  dfeu  2599  eu2  2613  eu4  2619  2mos  2653  2eu4  2658  r3ex  3178  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  reu2  3666  reu6  3667  reu4  3672  reu7  3673  rmo3f  3675  rmo4f  3676  2reu5lem3  3698  2reu5  3699  sbcimdv  3791  sbcg  3795  rmo3  3821  reuan  3828  dfpss2  4019  difdif  4065  raldifb  4079  inass  4156  dfss4  4197  dfin2  4199  indi  4212  indifdi  4222  undif3  4228  difin0ss  4301  inssdif0  4302  2nreu  4372  2reu4lem  4451  rexdifpr  4591  reuprg0  4634  ssdifsn  4721  ssunpr  4765  uniprg  4854  uniun  4861  uniin  4862  csbuni  4868  dfiun2g  4959  iunin2  5000  iundif2  5003  iindif2  5006  iinin2  5007  elpwpw  5031  axrep1  5200  axrep4v  5204  axrep4  5205  axrep4OLD  5206  reusv2lem4  5330  eqvinop  5427  opcom  5442  fconstmpt  5680  opeliunxp  5685  opeliun2xp  5686  xpundi  5687  elvvv  5694  opelinxp  5698  xpiindi  5777  elcnv2  5819  cnvuni  5828  dmuni  5856  brres  5938  dmres  5964  elidinxp  5996  restidsing  6005  elima3  6019  asymref  6066  imainss  6105  difxp  6115  xpdifid  6119  mptpreima  6189  coundir  6199  resco  6201  coass  6217  relrelss  6224  opreu2reurex  6245  dfpo2  6247  frpoind  6293  ordtri3or  6342  dffun2  6495  dffun6  6496  dffun3  6497  dffun4  6498  dffun5  6499  dffun6f  6500  dffun7  6512  dffun8  6513  dffun9  6514  svrelfun  6557  fncnv  6558  imadif  6569  dfmpt3  6619  fcnvres  6704  fint  6706  fin  6707  dff12  6722  fores  6749  dff1o4  6775  eqfnfv3  6973  fndmin  6986  fniniseg  7001  unpreima  7004  ffnfvf  7061  fsn2  7078  tpres  7145  fconstfv  7156  dff13f  7199  dff14a  7214  dff14b  7215  isocnv2  7275  f1opr  7412  eloprabga  7465  ffnov  7482  eqfnov  7485  foov  7530  uniuni  7705  tfindsg  7801  findsg  7837  funcnvuni  7872  opabex3d  7907  opabex3rd  7908  opabex3  7909  1stconst  8039  2ndconst  8040  frxp  8066  soxp  8069  xpord3lem  8089  suppvalbr  8104  suppofssd  8143  suppcoss  8147  mpoxopovel  8160  brtpos  8175  tpostpos  8186  dfsmo2  8277  dfrecs3  8302  rdglem1  8344  tz7.49  8374  brwitnlem  8432  oeeu  8529  naddasslem2  8621  brinxper  8663  erinxp  8728  mapsncnv  8831  cbvixp  8852  cbvixpv  8853  ixpin  8861  ixpiin  8862  mptelixpg  8873  elixpsn  8875  ixpsnf1o  8876  xpassen  8999  omxpenlem  9006  sbthcl  9027  sbthfilem  9122  wemapsolem  9455  dford2  9532  inf2  9535  zfinf  9551  ttrclselem2  9638  trcl  9640  frind  9665  frr3g  9671  iscard2  9891  leweon  9924  aceq1  10030  dfac3  10034  dfac4  10035  dfac5lem2  10037  dfac5  10042  kmlem3  10066  kmlem4  10067  kmlem14  10077  kmlem15  10078  dfackm  10080  infmap2  10130  fin23lem25  10237  zorn2lem7  10415  brdom6disj  10445  zfcndrep  10528  zfcndinf  10532  fpwwe  10560  axgroth4  10746  grothprim  10748  grothtsk  10749  nqpr  10928  addsrmo  10987  mulsrmo  10988  opelreal  11044  elnnz  12525  elznn0nn  12529  peano2uz2  12608  nnwos  12856  dflt2  13090  xmullem  13207  4fvwrd4  13593  preduz  13595  elfznelfzo  13719  fzind2  13734  fsuppmapnn0fiubex  13945  hashinfxadd  14338  hashgt23el  14377  hashfun  14390  fi1uzind  14460  brfi1uzind  14461  opfi1uzind  14464  cotr2g  14929  shftdm  15024  rexfiuz  15301  cbvsum  15648  cbvsumv  15649  mertenslem2  15841  mertens  15842  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  prodmo  15892  iprodmul  15959  divalglem10  16362  ndvdssub  16369  bitsmod  16396  algcvgblem  16537  isprm2  16642  isprm4  16644  hashdvds  16736  infpn2  16875  hashbc0  16967  xpscf  17520  funcpropd  17860  isffth2  17876  eldmcoa  18023  setcinv  18048  xpccatid  18145  yonedainv  18238  ispos  18271  ispos2  18272  joinfval2  18329  meetfval2  18343  istsr2  18541  isnsg2  19122  isnsg4  19133  isgim  19228  oppgid  19322  oppgcntz  19330  symgfix2  19382  efgval2  19690  iscyg2  19848  dmdprdd  19967  subgdmdprd  20002  issrg  20160  oppr1  20321  opprunit  20348  opprirred  20393  isrnghm  20412  isrhm  20449  issubrng  20519  subsubrng2  20536  subsubrg2  20571  rngcinv  20609  ringcinv  20643  isdomn2  20683  isdomn2OLD  20684  islmim  21052  lbsextg  21155  lidlnz  21235  resubdrg  21583  unocv  21655  pjfval2  21684  islinds2  21788  opsrtoslem1  22031  mdetunilem8  22602  istop2g  22879  isbasis2g  22931  tgval2  22939  isclo2  23071  isnrm2  23341  is1stc2  23425  llyi  23457  isfbas2  23818  elfg  23854  ufinffr  23912  isfcls  23992  alexsubALTlem2  24031  alexsubALTlem3  24032  cnextcn  24050  ustfilxp  24196  iscusp2  24284  metustid  24537  isclmp  25082  iscvsp  25113  tcphcph  25222  iscau3  25263  caucfil  25268  mdegleb  26047  ellogdm  26621  dvdsflsumcom  27169  logfac2  27198  dchrelbas3  27219  dchrvmasumlema  27481  nosupno  27685  noinfno  27700  noinfbnd1lem1  27705  dmcuts  27801  made0  27873  mulsproplem5  28130  norecdiv  28200  elnnzs  28411  uzsind  28415  zsoring  28419  legtrid  28677  outpasch  28841  axcontlem5  29055  axcontlem6  29056  axcontlem7  29057  nb3grpr2  29470  iscplgr  29502  dfpth2  29815  pthdlem1  29852  wwlksnextinj  29985  usgr2wspthon  30054  rusgrnumwwlkl1  30057  isclwwlk  30072  clwwlkccatlem  30077  clwwlknon2x  30191  iseupthf1o  30290  frcond3  30357  frgr3v  30363  4cycl2vnunb  30378  frgrncvvdeqlem2  30388  fusgr2wsp2nb  30422  numclwlk1lem1  30457  hhcms  31292  isch3  31330  ocsh  31372  pjhtheu  31483  pjpreeq  31487  h1deoi  31638  h1dei  31639  eleigvec  32046  cvbr2  32372  cvnbtwn2  32376  cvnbtwn4  32378  mdsl2i  32411  cvmdi  32413  mdsymlem6  32497  cdj3lem3b  32529  mo5f  32576  nmo  32577  rexunirn  32579  dmrab  32584  difrab2  32585  disjunsn  32683  unipreima  32735  dfcnv2  32767  1stpreima  32799  isunit2  33321  lsmsnorb2  33475  prmidl0  33533  ssmxidl  33557  1arithufdlem4  33630  ressply1mon1p  33651  extdgfialglem1  33876  zarcls  34058  rhmpreimacnlem  34068  isrnsiga  34297  rossros  34364  omsmeas  34507  eulerpartlemr  34558  eulerpartlemgvv  34560  ballotlemodife  34682  plymulx  34732  signstfvneq0  34756  bnj251  34885  bnj252  34886  bnj257  34890  bnj290  34893  bnj1304  35001  bnj153  35062  bnj543  35075  bnj571  35088  bnj580  35095  bnj607  35098  bnj882  35108  bnj964  35125  bnj996  35138  bnj1033  35151  bnj1176  35187  bnj1186  35189  bnj1189  35191  bnj1204  35194  bnj1253  35199  bnj1452  35234  bnj1463  35237  dff15  35265  axprALT2  35290  fineqvrep  35295  fineqvac  35297  lfuhgr3  35348  cusgredgex2  35351  usgrgt2cycl  35358  2cycl2d  35367  dfacycgr1  35372  erdszelem9  35427  cvmlift2lem9  35539  cvmlift2lem13  35543  satfvsucsuc  35593  satfdm  35597  satf0  35600  fmlasucdisj  35627  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  elmthm  35804  axinfprim  35934  axacprim  35935  xpab  35954  dfso2  35983  dford5reg  36008  dfon2lem5  36013  dfon2  36018  brtxp2  36107  brpprod3a  36112  dfom5b  36138  brcart  36158  brimg  36163  funpartlem  36170  dfrecs2  36178  cgrxfr  36283  segletr  36342  sumeq2si  36430  prodeq2si  36432  cbvprodvw2  36475  trer  36544  fneval  36580  neifg  36599  df3nandALT1  36627  andnand1  36629  nandsym1  36650  weiunlem  36691  regsfromregtco  36766  mh-infprim2bi  36775  mh-infprim3bi  36776  bj-df-sb  36990  bj-dfsbc  36992  bj-eu3f  37194  bj-csbsnlem  37256  bj-snsetex  37316  bj-elsngl  37321  bj-snglc  37322  bj-restuni  37455  bj-dfmpoa  37476  bj-imdirco  37550  mptsnunlem  37700  icorempo  37713  isbasisrelowllem2  37718  relowlpssretop  37726  rdgeqoa  37732  difunieq  37736  dffinxpf  37747  nlpineqsn  37770  curf  37965  finixpnum  37972  ptrest  37986  poimirlem1  37988  poimirlem14  38001  poimirlem16  38003  poimirlem19  38006  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimir  38020  cnambfre  38035  itg2addnc  38041  ftc1anc  38068  opropabco  38091  isdrngo1  38323  keridl  38399  ispridlc  38437  selconj  38467  eldmres3  38650  eldmqsres  38660  cnvepres  38671  ecinn0  38720  alrmomorn  38725  moantr  38739  dfxrn2  38752  disjressuc2  38778  inxpxrn  38785  rnxrnres  38789  coss2cnvepres  38875  refrelredund4  39086  dferALTV2  39120  dfeldisj3  39178  dfpart2  39239  dfpeters2  39341  petseq  39343  prtlem70  39349  prtlem100  39351  prtlem15  39367  islshpat  39509  lcvbr2  39514  lcvbr3  39515  lcvnbtwn2  39519  ellkr  39581  cvrval2  39766  cvrnbtwn2  39767  cvrnbtwn3  39768  cvrnbtwn4  39771  ishlat2  39845  lplnexatN  40055  islvol5  40071  dath  40228  pclfinclN  40442  lhpexle3  40504  4atex2  40569  4atex2-0bOLDN  40571  isltrn2N  40612  cdleme0nex  40782  cdleme22b  40833  cdlemg17pq  41164  cdlemg19  41176  cdlemg21  41178  cdlemg33d  41201  dibopelvalN  41635  dibopelval2  41637  dib1dim  41657  dicelval2N  41674  diclspsn  41686  lcdlss  42111  mapd1o  42140  3factsumint2  42507  3factsumint3  42508  3factsumint  42510  hashnexinj  42613  sticksstones16  42647  sticksstones21  42652  unitscyglem3  42682  supinf  42726  fimgmcyclem  43019  eu6w  43126  mzpcompact2lem  43200  fz1eqin  43218  rexrabdioph  43239  expdiophlem1  43466  dford4  43474  fnwe2lem2  43496  fgraphopab  43648  dflim6  43709  onsucf1olem  43715  onsucrn  43716  nnoeomeqom  43757  faosnf0.11b  43871  ifpidg  43935  rp-fakeinunass  43959  rp-isfinite6  43962  dfsucon  43967  elinintrab  44021  elnonrel  44029  elmapintab  44040  dfrtrcl5  44073  imaiun1  44095  coiun1  44096  rfovcnvf1od  44448  andi3or  44468  uneqsn  44469  ntrneicls00  44533  rr-groth  44743  ismnushort  44745  rr-grothshortbi  44747  2sbc5g  44860  pm14.12  44865  2sb5nd  45004  uun2221  45256  uun2221p1  45257  uun2221p2  45258  2sb5ndVD  45353  2sb5ndALT  45375  modelaxreplem3  45424  iindif2f  45607  disjinfi  45639  climuz  46187  dfxlim2  46291  cncfshift  46317  dvnmul  46386  dvnprodlem2  46390  ismbl3  46429  ismbl4  46436  stoweidlem26  46469  stoweidlem35  46478  fourierdlem54  46603  fourierdlem83  46632  fourierdlem100  46649  fourierdlem104  46653  fourierdlem109  46658  fourierdlem112  46661  smfpimcc  47251  fcoresf1ob  47536  f1cof1b  47540  f1ocof1ob  47544  2reu8i  47576  dfdfat2  47591  ffnaov  47662  an4com24  47731  4an21  47733  iccpartiltu  47897  prproropf1olem0  47977  dfgric2  48406  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgprismgr4cycllem10  48595  grlimedgnedg  48622  2zrngmmgm  48743  rngcinvALTV  48767  ringcinvALTV  48801  pgrpgt2nabl  48857  islindeps  48944  lindslinindsimp1  48948  lindslinindsimp2  48954  ldepslinc  49000  blen1b  49079  coxp  49323  i0oii  49410  io1ii  49411  isthinc2  49910  isthinc3  49911  isthincd2  49927  istermc2  49965  istermc3  49966  dffun3f  50172  setrec1lem3  50179  elpglem3  50203  elpg  50204