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

Syntax hints:   ↔ 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:  anbi1ci  626  anbi12i  628  bianass  642  an42  657  anandir  677  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  an3andi  1481  an33rean  1482  anxordi  1522  cadcoma  1608  nic-mpALT  1668  nic-axALT  1670  3exdistr  1957  4exdistr  1958  19.27v  1986  19.27  2224  19.41  2232  2sb5  2275  dfsb7  2277  dfeumo  2534  mo4f  2564  eu3v  2567  eu6  2571  dfeu  2592  eu2  2606  eu4  2612  2mos  2646  2mosOLD  2647  2eu4  2652  r3ex  3195  ceqsex3v  3536  ceqsex4v  3537  ceqsex8v  3539  reu2  3733  reu6  3734  reu4  3739  reu7  3740  rmo3f  3742  rmo4f  3743  2reu5lem3  3765  2reu5  3766  sbcimdv  3864  sbcg  3869  rmo3  3897  reuan  3904  dfpss2  4097  difdif  4144  raldifb  4158  inass  4235  dfss4  4274  dfin2  4276  indi  4289  indifdi  4299  undif3  4305  difin0ss  4378  inssdif0  4379  2nreu  4449  2reu4lem  4527  rexdifpr  4663  reuprg0  4706  ssdifsn  4792  ssunpr  4838  uniprg  4927  uniun  4934  uniin  4935  csbuni  4940  dfiun2g  5034  iunin2  5075  iundif2  5078  iindif2  5081  iinin2  5082  elpwpw  5106  axrep1  5285  axrep4v  5289  axrep4  5290  axrep4OLD  5291  reusv2lem4  5406  eqvinop  5497  opcom  5510  fconstmpt  5750  opeliunxp  5755  xpundi  5756  elvvv  5763  opelinxp  5767  xpiindi  5848  elcnv2  5890  cnvuni  5899  dmuni  5927  brres  6006  dmres  6031  elidinxp  6063  restidsing  6072  elima3  6086  asymref  6138  imainss  6175  difxp  6185  xpdifid  6189  mptpreima  6259  coundir  6269  resco  6271  coass  6286  relrelss  6294  opreu2reurex  6315  dfpo2  6317  frpoind  6364  wfiOLD  6373  ordtri3or  6417  dffun2  6572  dffun2OLD  6573  dffun2OLDOLD  6574  dffun6  6575  dffun3  6576  dffun3OLD  6577  dffun4  6578  dffun5  6579  dffun6f  6580  dffun7  6594  dffun8  6595  dffun9  6596  svrelfun  6639  fncnv  6640  imadif  6651  dfmpt3  6702  fcnvres  6785  fint  6787  fin  6788  dff12  6803  fores  6830  dff1o4  6856  eqfnfv3  7052  fndmin  7064  fniniseg  7079  unpreima  7082  ffnfvf  7139  fsn2  7155  tpres  7220  fconstfv  7231  dff13f  7275  dff14a  7289  dff14b  7290  isocnv2  7350  f1opr  7488  eloprabga  7540  ffnov  7558  eqfnov  7561  foov  7606  uniuni  7780  tfindsg  7881  findsg  7919  funcnvuni  7954  opabex3d  7988  opabex3rd  7989  opabex3  7990  1stconst  8123  2ndconst  8124  frxp  8149  soxp  8152  xpord3lem  8172  suppvalbr  8187  suppofssd  8226  suppcoss  8230  mpoxopovel  8243  brtpos  8258  tpostpos  8269  dfsmo2  8385  dfrecs3  8410  dfrecs3OLD  8411  rdglem1  8453  tz7.49  8483  brwitnlem  8543  oeeu  8639  naddasslem2  8731  brinxper  8772  erinxp  8829  mapsncnv  8931  cbvixp  8952  cbvixpv  8953  ixpin  8961  ixpiin  8962  mptelixpg  8973  elixpsn  8975  ixpsnf1o  8976  xpassen  9104  omxpenlem  9111  sbthcl  9133  sbthfilem  9235  wemapsolem  9587  dford2  9657  inf2  9660  zfinf  9676  ttrclselem2  9763  trcl  9765  frind  9787  frr3g  9793  iscard2  10013  leweon  10048  aceq1  10154  dfac3  10158  dfac4  10159  dfac5lem2  10161  dfac5  10166  kmlem3  10190  kmlem4  10191  kmlem14  10201  kmlem15  10202  dfackm  10204  infmap2  10254  fin23lem25  10361  zorn2lem7  10539  brdom6disj  10569  zfcndrep  10651  zfcndinf  10655  fpwwe  10683  axgroth4  10869  grothprim  10871  grothtsk  10872  nqpr  11051  addsrmo  11110  mulsrmo  11111  opelreal  11167  elnnz  12620  elznn0nn  12624  peano2uz2  12703  nnwos  12954  dflt2  13186  xmullem  13302  4fvwrd4  13684  preduz  13686  elfznelfzo  13807  fzind2  13820  fsuppmapnn0fiubex  14029  hashinfxadd  14420  hashgt23el  14459  hashfun  14472  fi1uzind  14542  brfi1uzind  14543  opfi1uzind  14546  cotr2g  15011  shftdm  15106  rexfiuz  15382  cbvsum  15727  cbvsumv  15728  mertenslem2  15917  mertens  15918  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  prodmo  15968  iprodmul  16035  divalglem10  16435  ndvdssub  16442  bitsmod  16469  algcvgblem  16610  isprm2  16715  isprm4  16717  hashdvds  16808  infpn2  16946  hashbc0  17038  xpscf  17611  funcpropd  17953  isffth2  17969  eldmcoa  18118  setcinv  18143  xpccatid  18243  yonedainv  18337  ispos  18371  ispos2  18372  joinfval2  18431  meetfval2  18445  istsr2  18641  isnsg2  19186  isnsg4  19197  isgim  19292  oppgid  19389  oppgcntz  19397  symgfix2  19448  efgval2  19756  iscyg2  19914  dmdprdd  20033  subgdmdprd  20068  issrg  20205  oppr1  20366  opprunit  20393  opprirred  20438  isrnghm  20457  isrhm  20494  issubrng  20563  subsubrng2  20580  subsubrg2  20615  rngcinv  20653  ringcinv  20687  isdomn2  20727  isdomn2OLD  20728  islmim  21078  lbsextg  21181  lidlnz  21269  resubdrg  21643  unocv  21715  pjfval2  21746  islinds2  21850  opsrtoslem1  22096  mdetunilem8  22640  istop2g  22917  isbasis2g  22970  tgval2  22978  isclo2  23111  isnrm2  23381  is1stc2  23465  llyi  23497  isfbas2  23858  elfg  23894  ufinffr  23952  isfcls  24032  alexsubALTlem2  24071  alexsubALTlem3  24072  cnextcn  24090  ustfilxp  24236  iscusp2  24326  metustid  24582  isclmp  25143  iscvsp  25174  tcphcph  25284  iscau3  25325  caucfil  25330  mdegleb  26117  ellogdm  26695  dvdsflsumcom  27245  logfac2  27275  dchrelbas3  27296  dchrvmasumlema  27558  nosupno  27762  noinfno  27777  noinfbnd1lem1  27782  dmscut  27870  made0  27926  mulsproplem5  28160  norecdiv  28230  elnnzs  28401  uzsind  28405  legtrid  28613  outpasch  28777  axcontlem5  28997  axcontlem6  28998  axcontlem7  28999  nb3grpr2  29414  iscplgr  29446  pthdlem1  29798  wwlksnextinj  29928  usgr2wspthon  29994  rusgrnumwwlkl1  29997  isclwwlk  30012  clwwlkccatlem  30017  clwwlknon2x  30131  iseupthf1o  30230  frcond3  30297  frgr3v  30303  4cycl2vnunb  30318  frgrncvvdeqlem2  30328  fusgr2wsp2nb  30362  numclwlk1lem1  30397  hhcms  31231  isch3  31269  ocsh  31311  pjhtheu  31422  pjpreeq  31426  h1deoi  31577  h1dei  31578  eleigvec  31985  cvbr2  32311  cvnbtwn2  32315  cvnbtwn4  32317  mdsl2i  32350  cvmdi  32352  mdsymlem6  32436  cdj3lem3b  32468  mo5f  32516  nmo  32517  rexunirn  32519  dmrab  32524  difrab2  32525  disjunsn  32613  unipreima  32659  dfcnv2  32692  1stpreima  32721  isunit2  33229  lsmsnorb2  33399  prmidl0  33457  ssmxidl  33481  1arithufdlem4  33554  ressply1mon1p  33572  zarcls  33834  rhmpreimacnlem  33844  isrnsiga  34093  rossros  34160  omsmeas  34304  eulerpartlemr  34355  eulerpartlemgvv  34357  ballotlemodife  34478  plymulx  34541  signstfvneq0  34565  bnj251  34694  bnj252  34695  bnj257  34699  bnj290  34702  bnj1304  34811  bnj153  34872  bnj543  34885  bnj571  34898  bnj580  34905  bnj607  34908  bnj882  34918  bnj964  34935  bnj996  34948  bnj1033  34961  bnj1176  34997  bnj1186  34999  bnj1189  35001  bnj1204  35004  bnj1253  35009  bnj1452  35044  bnj1463  35047  dff15  35076  fineqvrep  35087  fineqvac  35089  lfuhgr3  35103  cusgredgex2  35106  usgrgt2cycl  35114  2cycl2d  35123  dfacycgr1  35128  erdszelem9  35183  cvmlift2lem9  35295  cvmlift2lem13  35299  satfvsucsuc  35349  satfdm  35353  satf0  35356  fmlasucdisj  35383  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  elmthm  35560  axinfprim  35685  axacprim  35686  xpab  35705  dfso2  35734  dford5reg  35763  dfon2lem5  35768  dfon2  35773  brtxp2  35862  brpprod3a  35867  dfom5b  35893  brcart  35913  brimg  35918  funpartlem  35923  dfrecs2  35931  cgrxfr  36036  segletr  36095  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36229  trer  36298  fneval  36334  neifg  36353  df3nandALT1  36381  andnand1  36383  nandsym1  36404  weiunlem2  36445  bj-eu3f  36823  bj-csbsnlem  36885  bj-snsetex  36945  bj-elsngl  36950  bj-snglc  36951  bj-restuni  37079  bj-dfmpoa  37100  bj-imdirco  37172  mptsnunlem  37320  icorempo  37333  isbasisrelowllem2  37338  relowlpssretop  37346  rdgeqoa  37352  difunieq  37356  dffinxpf  37367  nlpineqsn  37390  curf  37584  finixpnum  37591  ptrest  37605  poimirlem1  37607  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimir  37639  cnambfre  37654  itg2addnc  37660  ftc1anc  37687  opropabco  37710  isdrngo1  37942  keridl  38018  ispridlc  38056  selconj  38086  eldmqsres  38268  cnvepres  38279  ecinn0  38334  alrmomorn  38339  moantr  38345  dfxrn2  38357  disjressuc2  38369  inxpxrn  38376  rnxrnres  38380  coss2cnvepres  38399  refrelredund4  38616  dferALTV2  38649  dfeldisj3  38700  dfpart2  38750  prtlem70  38838  prtlem100  38840  prtlem15  38856  islshpat  38998  lcvbr2  39003  lcvbr3  39004  lcvnbtwn2  39008  ellkr  39070  cvrval2  39255  cvrnbtwn2  39256  cvrnbtwn3  39257  cvrnbtwn4  39260  ishlat2  39334  lplnexatN  39545  islvol5  39561  dath  39718  pclfinclN  39932  lhpexle3  39994  4atex2  40059  4atex2-0bOLDN  40061  isltrn2N  40102  cdleme0nex  40272  cdleme22b  40323  cdlemg17pq  40654  cdlemg19  40666  cdlemg21  40668  cdlemg33d  40691  dibopelvalN  41125  dibopelval2  41127  dib1dim  41147  dicelval2N  41164  diclspsn  41176  lcdlss  41601  mapd1o  41630  3factsumint2  42003  3factsumint3  42004  3factsumint  42006  hashnexinj  42109  sticksstones16  42143  sticksstones21  42148  unitscyglem3  42178  metakunt1  42186  supinf  42261  fimgmcyclem  42519  eu6w  42662  mzpcompact2lem  42738  fz1eqin  42756  rexrabdioph  42781  expdiophlem1  43009  dford4  43017  fnwe2lem2  43039  fgraphopab  43191  dflim6  43253  onsucf1olem  43259  onsucrn  43260  nnoeomeqom  43301  faosnf0.11b  43416  ifpidg  43480  rp-fakeinunass  43504  rp-isfinite6  43507  dfsucon  43512  elinintrab  43566  elnonrel  43574  elmapintab  43585  dfrtrcl5  43618  imaiun1  43640  coiun1  43641  rfovcnvf1od  43993  andi3or  44013  uneqsn  44014  ntrneicls00  44078  rr-groth  44294  ismnushort  44296  rr-grothshortbi  44298  2sbc5g  44411  pm14.12  44416  2sb5nd  44557  uun2221  44810  uun2221p1  44811  uun2221p2  44812  2sb5ndVD  44907  2sb5ndALT  44929  modelaxreplem3  44944  iindif2f  45102  disjinfi  45134  climuz  45699  dfxlim2  45803  cncfshift  45829  dvnmul  45898  dvnprodlem2  45902  ismbl3  45941  ismbl4  45948  stoweidlem26  45981  stoweidlem35  45990  fourierdlem54  46115  fourierdlem83  46144  fourierdlem100  46161  fourierdlem104  46165  fourierdlem109  46170  fourierdlem112  46173  smfpimcc  46763  fcoresf1ob  47022  f1cof1b  47026  f1ocof1ob  47030  2reu8i  47062  dfdfat2  47077  ffnaov  47148  an4com24  47217  4an21  47219  iccpartiltu  47346  prproropf1olem0  47426  dfgric2  47821  gpgvtxedg0  47955  gpgvtxedg1  47956  2zrngmmgm  48095  rngcinvALTV  48119  ringcinvALTV  48153  opeliun2xp  48177  pgrpgt2nabl  48210  islindeps  48298  lindslinindsimp1  48302  lindslinindsimp2  48308  ldepslinc  48354  blen1b  48437  i0oii  48715  io1ii  48716  iscnrm3lem3  48731  isthinc2  48821  isthinc3  48822  isthincd2  48837  dffun3f  48912  setrec1lem3  48919  elpglem3  48943  elpg  48944