Theorem anbi2i 623

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 575	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  anbi1ci  626  anbi12i  627  bianass  639  an42  654  anandir  674  dfbi3  1047  dn1  1055  dfifp3  1063  ifpdfbi  1068  an3andi  1481  an33rean  1482  an33reanOLD  1483  anxordi  1523  norassOLD  1536  cadcoma  1614  nic-mpALT  1675  nic-axALT  1677  3exdistr  1965  4exdistr  1966  19.27v  1994  19.27  2221  19.41  2229  2sb5  2273  dfsb7  2277  dfeumo  2538  mo4f  2568  eu3v  2571  eu6  2575  dfeu  2596  eu2  2612  eu4  2618  2mos  2652  2eu4  2657  ceqsex3v  3485  ceqsex4v  3486  ceqsex8v  3488  reu2  3661  reu6  3662  reu4  3667  reu7  3668  rmo3f  3670  rmo4f  3671  2reu5lem3  3693  2reu5  3694  sbcimdv  3791  sbcg  3796  rmo3  3823  reuan  3830  dfpss2  4021  difdif  4066  raldifb  4080  inass  4154  dfss4  4193  dfin2  4195  indi  4208  indifdi  4218  indifdirOLD  4220  undif3  4225  difin0ss  4303  inssdif0  4304  2nreu  4376  2reu4lem  4457  rexdifpr  4595  reuprg0  4639  ssdifsn  4722  ssunpr  4766  uniprg  4857  uniprOLD  4859  uniun  4865  uniin  4866  csbuni  4871  dfiun2g  4961  iunin2  5001  iundif2  5004  iindif2  5007  iinin2  5008  elpwpw  5032  axrep1  5211  axrep4  5215  reusv2lem4  5325  eqvinop  5402  opcom  5416  fconstmpt  5650  opeliunxp  5655  xpundi  5656  elvvv  5663  opelinxp  5667  xpiindi  5747  elcnv2  5789  cnvuni  5798  dmuni  5826  brres  5901  dmres  5916  elidinxp  5954  restidsing  5965  elima3  5979  asymref  6026  imainss  6062  difxp  6072  xpdifid  6076  mptpreima  6146  coundir  6156  resco  6158  coass  6173  relrelss  6180  opreu2reurex  6201  dfpo2  6203  frpoind  6249  wfiOLD  6258  ordtri3or  6302  dffun2  6447  dffun2OLD  6448  dffun6  6449  dffun3  6450  dffun3OLD  6451  dffun4  6452  dffun5  6453  dffun6f  6454  dffun7  6468  dffun8  6469  dffun9  6470  svrelfun  6513  fncnv  6514  imadif  6525  dfmpt3  6576  fcnvres  6660  fint  6662  fin  6663  dff12  6678  fores  6707  dff1o4  6733  eqfnfv3  6920  fndmin  6931  fniniseg  6946  unpreima  6949  ffnfvf  7002  fsn2  7017  tpres  7085  fconstfv  7097  dff13f  7138  dff14a  7152  dff14b  7153  isocnv2  7211  f1opr  7340  eloprabga  7391  ffnov  7410  eqfnov  7412  foov  7455  uniuni  7621  tfindsg  7716  findsg  7755  funcnvuni  7787  opabex3d  7817  opabex3rd  7818  opabex3  7819  1stconst  7949  2ndconst  7950  frxp  7976  soxp  7979  suppvalbr  7990  suppofssd  8028  suppcoss  8032  mpoxopovel  8045  brtpos  8060  tpostpos  8071  dfsmo2  8187  dfrecs3  8212  dfrecs3OLD  8213  rdglem1  8255  tz7.49  8285  brwitnlem  8346  oeeu  8443  erinxp  8589  mapsncnv  8690  cbvixp  8711  ixpin  8720  ixpiin  8721  mptelixpg  8732  elixpsn  8734  ixpsnf1o  8735  xpassen  8862  omxpenlem  8869  sbthcl  8891  sbthfilem  8993  wemapsolem  9318  dford2  9387  inf2  9390  zfinf  9406  ttrclselem2  9493  trcl  9495  frind  9517  frr3g  9523  iscard2  9743  leweon  9776  aceq1  9882  dfac3  9886  dfac4  9887  dfac5lem2  9889  dfac5  9893  kmlem3  9917  kmlem4  9918  kmlem14  9928  kmlem15  9929  dfackm  9931  infmap2  9983  fin23lem25  10089  zorn2lem7  10267  brdom6disj  10297  zfcndrep  10379  zfcndinf  10383  fpwwe  10411  axgroth4  10597  grothprim  10599  grothtsk  10600  nqpr  10779  addsrmo  10838  mulsrmo  10839  opelreal  10895  elnnz  12338  elznn0nn  12342  peano2uz2  12417  nnwos  12664  dflt2  12891  xmullem  13007  4fvwrd4  13385  preduz  13387  elfznelfzo  13501  fzind2  13514  fsuppmapnn0fiubex  13721  hashinfxadd  14109  hashgt23el  14148  hashfun  14161  fi1uzind  14220  brfi1uzind  14221  opfi1uzind  14224  cotr2g  14696  shftdm  14791  rexfiuz  15068  cbvsum  15416  mertenslem2  15606  mertens  15607  cbvprod  15634  prodmo  15655  iprodmul  15722  divalglem10  16120  ndvdssub  16127  bitsmod  16152  algcvgblem  16291  isprm2  16396  isprm4  16398  hashdvds  16485  infpn2  16623  hashbc0  16715  xpscf  17285  funcpropd  17625  isffth2  17641  eldmcoa  17789  setcinv  17814  xpccatid  17914  yonedainv  18008  ispos  18041  ispos2  18042  joinfval2  18101  meetfval2  18115  istsr2  18311  isnsg2  18793  isnsg4  18804  isgim  18887  oppgid  18972  oppgcntz  18980  symgfix2  19033  efgval2  19339  iscyg2  19491  dmdprdd  19611  subgdmdprd  19646  issrg  19752  oppr1  19885  opprunit  19912  opprirred  19953  isrhm  19974  subsubrg2  20060  islmim  20333  lbsextg  20433  lidlnz  20508  isdomn2  20579  resubdrg  20822  unocv  20894  pjfval2  20925  islinds2  21029  opsrtoslem1  21271  mdetunilem8  21777  istop2g  22054  isbasis2g  22107  tgval2  22115  isclo2  22248  isnrm2  22518  is1stc2  22602  llyi  22634  isfbas2  22995  elfg  23031  ufinffr  23089  isfcls  23169  alexsubALTlem2  23208  alexsubALTlem3  23209  cnextcn  23227  ustfilxp  23373  iscusp2  23463  metustid  23719  isclmp  24269  iscvsp  24300  tcphcph  24410  iscau3  24451  caucfil  24456  mdegleb  25238  ellogdm  25803  dvdsflsumcom  26346  logfac2  26374  dchrelbas3  26395  dchrvmasumlema  26657  legtrid  26961  outpasch  27125  axcontlem5  27345  axcontlem6  27346  axcontlem7  27347  nb3grpr2  27759  iscplgr  27791  pthdlem1  28143  wwlksnextinj  28273  usgr2wspthon  28339  rusgrnumwwlkl1  28342  isclwwlk  28357  clwwlkccatlem  28362  clwwlknon2x  28476  iseupthf1o  28575  frcond3  28642  frgr3v  28648  4cycl2vnunb  28663  frgrncvvdeqlem2  28673  fusgr2wsp2nb  28707  numclwlk1lem1  28742  hhcms  29574  isch3  29612  ocsh  29654  pjhtheu  29765  pjpreeq  29769  h1deoi  29920  h1dei  29921  eleigvec  30328  cvbr2  30654  cvnbtwn2  30658  cvnbtwn4  30660  mdsl2i  30693  cvmdi  30695  mdsymlem6  30779  cdj3lem3b  30811  mo5f  30846  nmo  30847  rexunirn  30849  dmrab  30853  difrab2  30854  disjunsn  30942  unipreima  30990  dfcnv2  31022  1stpreima  31048  lsmsnorb2  31589  prmidl0  31635  ssmxidl  31651  zarcls  31833  rhmpreimacnlem  31843  isrnsiga  32090  rossros  32157  omsmeas  32299  eulerpartlemr  32350  eulerpartlemgvv  32352  ballotlemodife  32473  plymulx  32536  signstfvneq0  32560  bnj251  32690  bnj252  32691  bnj257  32695  bnj290  32698  bnj1304  32808  bnj153  32869  bnj543  32882  bnj571  32895  bnj580  32902  bnj607  32905  bnj882  32915  bnj964  32932  bnj996  32945  bnj1033  32958  bnj1176  32994  bnj1186  32996  bnj1189  32998  bnj1204  33001  bnj1253  33006  bnj1452  33041  bnj1463  33044  dff15  33065  fineqvrep  33073  fineqvac  33075  lfuhgr3  33090  cusgredgex2  33093  usgrgt2cycl  33101  2cycl2d  33110  dfacycgr1  33115  erdszelem9  33170  cvmlift2lem9  33282  cvmlift2lem13  33286  satfvsucsuc  33336  satfdm  33340  satf0  33343  fmlasucdisj  33370  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  elmthm  33547  axinfprim  33656  axacprim  33657  xpab  33686  dfso2  33731  dford5reg  33767  dfon2lem5  33772  dfon2  33777  xpord3lem  33804  nosupno  33915  noinfno  33930  noinfbnd1lem1  33935  dmscut  34014  made0  34066  brtxp2  34192  brpprod3a  34197  dfom5b  34223  brcart  34243  brimg  34248  funpartlem  34253  dfrecs2  34261  cgrxfr  34366  segletr  34425  trer  34514  fneval  34550  neifg  34569  df3nandALT1  34597  andnand1  34599  nandsym1  34620  bj-eu3f  35034  bj-csbsnlem  35097  bj-snsetex  35162  bj-elsngl  35167  bj-snglc  35168  bj-restuni  35277  bj-dfmpoa  35298  bj-imdirco  35370  mptsnunlem  35518  icorempo  35531  isbasisrelowllem2  35536  relowlpssretop  35544  rdgeqoa  35550  difunieq  35554  dffinxpf  35565  nlpineqsn  35588  curf  35764  finixpnum  35771  ptrest  35785  poimirlem1  35787  poimirlem14  35800  poimirlem16  35802  poimirlem19  35805  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimir  35819  cnambfre  35834  itg2addnc  35840  ftc1anc  35867  opropabco  35891  isdrngo1  36123  keridl  36199  ispridlc  36237  selconj  36267  eldmqsres  36429  cnvepres  36441  ecinn0  36492  alrmomorn  36497  moantr  36501  dfxrn2  36513  inxpxrn  36528  rnxrnres  36532  refrelredund4  36755  dferALTV2  36787  dfeldisj3  36837  prtlem70  36878  prtlem100  36880  prtlem15  36896  islshpat  37038  lcvbr2  37043  lcvbr3  37044  lcvnbtwn2  37048  ellkr  37110  cvrval2  37295  cvrnbtwn2  37296  cvrnbtwn3  37297  cvrnbtwn4  37300  ishlat2  37374  lplnexatN  37584  islvol5  37600  dath  37757  pclfinclN  37971  lhpexle3  38033  4atex2  38098  4atex2-0bOLDN  38100  isltrn2N  38141  cdleme0nex  38311  cdleme22b  38362  cdlemg17pq  38693  cdlemg19  38705  cdlemg21  38707  cdlemg33d  38730  dibopelvalN  39164  dibopelval2  39166  dib1dim  39186  dicelval2N  39203  diclspsn  39215  lcdlss  39640  mapd1o  39669  3factsumint2  40037  3factsumint3  40038  3factsumint  40040  sticksstones16  40125  sticksstones21  40130  metakunt1  40132  mhphf  40292  prjcrv0  40477  mzpcompact2lem  40580  fz1eqin  40598  rexrabdioph  40623  expdiophlem1  40850  dford4  40858  fnwe2lem2  40883  fgraphopab  41042  ifpidg  41105  rp-fakeinunass  41129  rp-isfinite6  41132  dfsucon  41137  elinintrab  41192  elnonrel  41200  elmapintab  41211  dfrtrcl5  41244  imaiun1  41266  coiun1  41267  rfovcnvf1od  41619  andi3or  41639  uneqsn  41640  ntrneicls00  41706  rr-groth  41924  ismnushort  41926  rr-grothshortbi  41928  2sbc5g  42041  pm14.12  42046  2sb5nd  42187  uun2221  42440  uun2221p1  42441  uun2221p2  42442  2sb5ndVD  42537  2sb5ndALT  42559  disjinfi  42738  climuz  43292  dfxlim2  43396  cncfshift  43422  dvnmul  43491  dvnprodlem2  43495  ismbl3  43534  ismbl4  43541  stoweidlem26  43574  stoweidlem35  43583  fourierdlem54  43708  fourierdlem83  43737  fourierdlem100  43754  fourierdlem104  43758  fourierdlem109  43763  fourierdlem112  43766  smfpimcc  44352  fcoresf1ob  44578  f1cof1b  44580  f1ocof1ob  44584  2reu8i  44616  dfdfat2  44631  ffnaov  44702  an4com24  44771  4an21  44773  iccpartiltu  44885  prproropf1olem0  44965  isrnghm  45461  2zrngmmgm  45515  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  opeliun2xp  45679  pgrpgt2nabl  45713  islindeps  45805  lindslinindsimp1  45809  lindslinindsimp2  45815  ldepslinc  45861  blen1b  45945  i0oii  46224  io1ii  46225  iscnrm3lem3  46240  isthinc2  46314  isthinc3  46315  isthincd2  46330  dffun3f  46399  setrec1lem3  46406  elpglem3  46429  elpg  46430