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  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1527  cadcoma  1613  nic-mpALT  1673  nic-axALT  1675  3exdistr  1961  4exdistr  1962  19.27v  1996  19.27  2234  19.41  2242  2sb5  2284  dfsb7  2285  dfeumo  2536  mo4f  2567  eu3v  2570  eu6  2574  dfeu  2595  eu2  2609  eu4  2615  2mos  2649  2mosOLD  2650  2eu4  2655  r3ex  3175  ceqsex3v  3495  ceqsex4v  3496  ceqsex8v  3498  reu2  3683  reu6  3684  reu4  3689  reu7  3690  rmo3f  3692  rmo4f  3693  2reu5lem3  3715  2reu5  3716  sbcimdv  3809  sbcg  3813  rmo3  3839  reuan  3846  dfpss2  4040  difdif  4087  raldifb  4101  inass  4180  dfss4  4221  dfin2  4223  indi  4236  indifdi  4246  undif3  4252  difin0ss  4325  inssdif0  4326  2nreu  4396  2reu4lem  4476  rexdifpr  4616  reuprg0  4659  ssdifsn  4744  ssunpr  4790  uniprg  4879  uniun  4886  uniin  4887  csbuni  4893  dfiun2g  4985  iunin2  5026  iundif2  5029  iindif2  5032  iinin2  5033  elpwpw  5057  axrep1  5225  axrep4v  5229  axrep4  5230  axrep4OLD  5231  reusv2lem4  5346  eqvinop  5435  opcom  5449  fconstmpt  5686  opeliunxp  5691  opeliun2xp  5692  xpundi  5693  elvvv  5700  opelinxp  5704  xpiindi  5784  elcnv2  5826  cnvuni  5835  dmuni  5863  brres  5945  dmres  5971  elidinxp  6003  restidsing  6012  elima3  6026  asymref  6073  imainss  6112  difxp  6122  xpdifid  6126  mptpreima  6196  coundir  6206  resco  6208  coass  6224  relrelss  6231  opreu2reurex  6252  dfpo2  6254  frpoind  6300  ordtri3or  6349  dffun2  6502  dffun6  6503  dffun3  6504  dffun4  6505  dffun5  6506  dffun6f  6507  dffun7  6519  dffun8  6520  dffun9  6521  svrelfun  6564  fncnv  6565  imadif  6576  dfmpt3  6626  fcnvres  6711  fint  6713  fin  6714  dff12  6729  fores  6756  dff1o4  6782  eqfnfv3  6978  fndmin  6990  fniniseg  7005  unpreima  7008  ffnfvf  7065  fsn2  7081  tpres  7147  fconstfv  7158  dff13f  7201  dff14a  7216  dff14b  7217  isocnv2  7277  f1opr  7414  eloprabga  7467  ffnov  7484  eqfnov  7487  foov  7532  uniuni  7707  tfindsg  7803  findsg  7839  funcnvuni  7874  opabex3d  7909  opabex3rd  7910  opabex3  7911  1stconst  8042  2ndconst  8043  frxp  8068  soxp  8071  xpord3lem  8091  suppvalbr  8106  suppofssd  8145  suppcoss  8149  mpoxopovel  8162  brtpos  8177  tpostpos  8188  dfsmo2  8279  dfrecs3  8304  rdglem1  8346  tz7.49  8376  brwitnlem  8434  oeeu  8531  naddasslem2  8623  brinxper  8664  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  9529  inf2  9532  zfinf  9548  ttrclselem2  9635  trcl  9637  frind  9662  frr3g  9668  iscard2  9888  leweon  9921  aceq1  10027  dfac3  10031  dfac4  10032  dfac5lem2  10034  dfac5  10039  kmlem3  10063  kmlem4  10064  kmlem14  10074  kmlem15  10075  dfackm  10077  infmap2  10127  fin23lem25  10234  zorn2lem7  10412  brdom6disj  10442  zfcndrep  10525  zfcndinf  10529  fpwwe  10557  axgroth4  10743  grothprim  10745  grothtsk  10746  nqpr  10925  addsrmo  10984  mulsrmo  10985  opelreal  11041  elnnz  12498  elznn0nn  12502  peano2uz2  12580  nnwos  12828  dflt2  13062  xmullem  13179  4fvwrd4  13564  preduz  13566  elfznelfzo  13689  fzind2  13704  fsuppmapnn0fiubex  13915  hashinfxadd  14308  hashgt23el  14347  hashfun  14360  fi1uzind  14430  brfi1uzind  14431  opfi1uzind  14434  cotr2g  14899  shftdm  14994  rexfiuz  15271  cbvsum  15618  cbvsumv  15619  mertenslem2  15808  mertens  15809  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  prodmo  15859  iprodmul  15926  divalglem10  16329  ndvdssub  16336  bitsmod  16363  algcvgblem  16504  isprm2  16609  isprm4  16611  hashdvds  16702  infpn2  16841  hashbc0  16933  xpscf  17486  funcpropd  17826  isffth2  17842  eldmcoa  17989  setcinv  18014  xpccatid  18111  yonedainv  18204  ispos  18237  ispos2  18238  joinfval2  18295  meetfval2  18309  istsr2  18507  isnsg2  19085  isnsg4  19096  isgim  19191  oppgid  19285  oppgcntz  19293  symgfix2  19345  efgval2  19653  iscyg2  19811  dmdprdd  19930  subgdmdprd  19965  issrg  20123  oppr1  20286  opprunit  20313  opprirred  20358  isrnghm  20377  isrhm  20414  issubrng  20480  subsubrng2  20497  subsubrg2  20532  rngcinv  20570  ringcinv  20604  isdomn2  20644  isdomn2OLD  20645  islmim  21014  lbsextg  21117  lidlnz  21197  resubdrg  21563  unocv  21635  pjfval2  21664  islinds2  21768  opsrtoslem1  22010  mdetunilem8  22563  istop2g  22840  isbasis2g  22892  tgval2  22900  isclo2  23032  isnrm2  23302  is1stc2  23386  llyi  23418  isfbas2  23779  elfg  23815  ufinffr  23873  isfcls  23953  alexsubALTlem2  23992  alexsubALTlem3  23993  cnextcn  24011  ustfilxp  24157  iscusp2  24245  metustid  24498  isclmp  25053  iscvsp  25084  tcphcph  25193  iscau3  25234  caucfil  25239  mdegleb  26025  ellogdm  26604  dvdsflsumcom  27154  logfac2  27184  dchrelbas3  27205  dchrvmasumlema  27467  nosupno  27671  noinfno  27686  noinfbnd1lem1  27691  dmcuts  27787  made0  27859  mulsproplem5  28116  norecdiv  28186  elnnzs  28397  uzsind  28401  zsoring  28405  legtrid  28663  outpasch  28827  axcontlem5  29041  axcontlem6  29042  axcontlem7  29043  nb3grpr2  29456  iscplgr  29488  dfpth2  29802  pthdlem1  29839  wwlksnextinj  29972  usgr2wspthon  30041  rusgrnumwwlkl1  30044  isclwwlk  30059  clwwlkccatlem  30064  clwwlknon2x  30178  iseupthf1o  30277  frcond3  30344  frgr3v  30350  4cycl2vnunb  30365  frgrncvvdeqlem2  30375  fusgr2wsp2nb  30409  numclwlk1lem1  30444  hhcms  31278  isch3  31316  ocsh  31358  pjhtheu  31469  pjpreeq  31473  h1deoi  31624  h1dei  31625  eleigvec  32032  cvbr2  32358  cvnbtwn2  32362  cvnbtwn4  32364  mdsl2i  32397  cvmdi  32399  mdsymlem6  32483  cdj3lem3b  32515  mo5f  32563  nmo  32564  rexunirn  32566  dmrab  32571  difrab2  32572  disjunsn  32669  unipreima  32721  dfcnv2  32754  1stpreima  32786  isunit2  33322  lsmsnorb2  33473  prmidl0  33531  ssmxidl  33555  1arithufdlem4  33628  ressply1mon1p  33649  extdgfialglem1  33849  zarcls  34031  rhmpreimacnlem  34041  isrnsiga  34270  rossros  34337  omsmeas  34480  eulerpartlemr  34531  eulerpartlemgvv  34533  ballotlemodife  34655  plymulx  34705  signstfvneq0  34729  bnj251  34858  bnj252  34859  bnj257  34863  bnj290  34866  bnj1304  34975  bnj153  35036  bnj543  35049  bnj571  35062  bnj580  35069  bnj607  35072  bnj882  35082  bnj964  35099  bnj996  35112  bnj1033  35125  bnj1176  35161  bnj1186  35163  bnj1189  35165  bnj1204  35168  bnj1253  35173  bnj1452  35208  bnj1463  35211  dff15  35240  fineqvrep  35270  fineqvac  35272  lfuhgr3  35314  cusgredgex2  35317  usgrgt2cycl  35324  2cycl2d  35333  dfacycgr1  35338  erdszelem9  35393  cvmlift2lem9  35505  cvmlift2lem13  35509  satfvsucsuc  35559  satfdm  35563  satf0  35566  fmlasucdisj  35593  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  elmthm  35770  axinfprim  35900  axacprim  35901  xpab  35920  dfso2  35949  dford5reg  35974  dfon2lem5  35979  dfon2  35984  brtxp2  36073  brpprod3a  36078  dfom5b  36104  brcart  36124  brimg  36129  funpartlem  36136  dfrecs2  36144  cgrxfr  36249  segletr  36308  sumeq2si  36396  prodeq2si  36398  cbvprodvw2  36441  trer  36510  fneval  36546  neifg  36565  df3nandALT1  36593  andnand1  36595  nandsym1  36616  weiunlem  36657  regsfromregtr  36668  bj-df-sb  36853  bj-eu3f  37042  bj-csbsnlem  37104  bj-snsetex  37164  bj-elsngl  37169  bj-snglc  37170  bj-restuni  37302  bj-dfmpoa  37323  bj-imdirco  37395  mptsnunlem  37543  icorempo  37556  isbasisrelowllem2  37561  relowlpssretop  37569  rdgeqoa  37575  difunieq  37579  dffinxpf  37590  nlpineqsn  37613  curf  37799  finixpnum  37806  ptrest  37820  poimirlem1  37822  poimirlem14  37835  poimirlem16  37837  poimirlem19  37840  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimir  37854  cnambfre  37869  itg2addnc  37875  ftc1anc  37902  opropabco  37925  isdrngo1  38157  keridl  38233  ispridlc  38271  selconj  38301  eldmres3  38476  eldmqsres  38486  cnvepres  38497  ecinn0  38546  alrmomorn  38551  moantr  38557  dfxrn2  38570  disjressuc2  38596  inxpxrn  38603  rnxrnres  38607  coss2cnvepres  38681  refrelredund4  38892  dfblockliftfix2  38897  dferALTV2  38927  dfeldisj3  38978  dfpart2  39028  prtlem70  39117  prtlem100  39119  prtlem15  39135  islshpat  39277  lcvbr2  39282  lcvbr3  39283  lcvnbtwn2  39287  ellkr  39349  cvrval2  39534  cvrnbtwn2  39535  cvrnbtwn3  39536  cvrnbtwn4  39539  ishlat2  39613  lplnexatN  39823  islvol5  39839  dath  39996  pclfinclN  40210  lhpexle3  40272  4atex2  40337  4atex2-0bOLDN  40339  isltrn2N  40380  cdleme0nex  40550  cdleme22b  40601  cdlemg17pq  40932  cdlemg19  40944  cdlemg21  40946  cdlemg33d  40969  dibopelvalN  41403  dibopelval2  41405  dib1dim  41425  dicelval2N  41442  diclspsn  41454  lcdlss  41879  mapd1o  41908  3factsumint2  42276  3factsumint3  42277  3factsumint  42279  hashnexinj  42382  sticksstones16  42416  sticksstones21  42421  unitscyglem3  42451  supinf  42497  fimgmcyclem  42788  eu6w  42919  mzpcompact2lem  42993  fz1eqin  43011  rexrabdioph  43036  expdiophlem1  43263  dford4  43271  fnwe2lem2  43293  fgraphopab  43445  dflim6  43506  onsucf1olem  43512  onsucrn  43513  nnoeomeqom  43554  faosnf0.11b  43668  ifpidg  43732  rp-fakeinunass  43756  rp-isfinite6  43759  dfsucon  43764  elinintrab  43818  elnonrel  43826  elmapintab  43837  dfrtrcl5  43870  imaiun1  43892  coiun1  43893  rfovcnvf1od  44245  andi3or  44265  uneqsn  44266  ntrneicls00  44330  rr-groth  44540  ismnushort  44542  rr-grothshortbi  44544  2sbc5g  44657  pm14.12  44662  2sb5nd  44801  uun2221  45053  uun2221p1  45054  uun2221p2  45055  2sb5ndVD  45150  2sb5ndALT  45172  modelaxreplem3  45221  iindif2f  45404  disjinfi  45436  climuz  45988  dfxlim2  46092  cncfshift  46118  dvnmul  46187  dvnprodlem2  46191  ismbl3  46230  ismbl4  46237  stoweidlem26  46270  stoweidlem35  46279  fourierdlem54  46404  fourierdlem83  46433  fourierdlem100  46450  fourierdlem104  46454  fourierdlem109  46459  fourierdlem112  46462  smfpimcc  47052  fcoresf1ob  47319  f1cof1b  47323  f1ocof1ob  47327  2reu8i  47359  dfdfat2  47374  ffnaov  47445  an4com24  47514  4an21  47516  iccpartiltu  47668  prproropf1olem0  47748  dfgric2  48161  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgprismgr4cycllem10  48350  grlimedgnedg  48377  2zrngmmgm  48498  rngcinvALTV  48522  ringcinvALTV  48556  pgrpgt2nabl  48612  islindeps  48699  lindslinindsimp1  48703  lindslinindsimp2  48709  ldepslinc  48755  blen1b  48834  coxp  49078  i0oii  49165  io1ii  49166  isthinc2  49665  isthinc3  49666  isthincd2  49682  istermc2  49720  istermc3  49721  dffun3f  49927  setrec1lem3  49934  elpglem3  49958  elpg  49959