Theorem anbi2i 624

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  627  anbi12i  629  bianass  643  an42  658  anandir  678  dfbi3  1050  dn1  1058  dfifp3  1066  ifpdfbi  1071  4anpull2  1363  an3andi  1485  an33rean  1486  anxordi  1528  cadcoma  1614  nic-mpALT  1674  nic-axALT  1676  3exdistr  1962  4exdistr  1963  19.27v  1997  19.27  2235  19.41  2243  2sb5  2285  dfsb7  2286  dfeumo  2537  mo4f  2568  eu3v  2571  eu6  2575  dfeu  2596  eu2  2610  eu4  2616  2mos  2650  2mosOLD  2651  2eu4  2656  r3ex  3177  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  reu2  3672  reu6  3673  reu4  3678  reu7  3679  rmo3f  3681  rmo4f  3682  2reu5lem3  3704  2reu5  3705  sbcimdv  3798  sbcg  3802  rmo3  3828  reuan  3835  dfpss2  4029  difdif  4076  raldifb  4090  inass  4169  dfss4  4210  dfin2  4212  indi  4225  indifdi  4235  undif3  4241  difin0ss  4314  inssdif0  4315  2nreu  4385  2reu4lem  4464  rexdifpr  4604  reuprg0  4647  ssdifsn  4732  ssunpr  4778  uniprg  4867  uniun  4874  uniin  4875  csbuni  4881  dfiun2g  4973  iunin2  5014  iundif2  5017  iindif2  5020  iinin2  5021  elpwpw  5045  axrep1  5214  axrep4v  5218  axrep4  5219  axrep4OLD  5220  reusv2lem4  5339  eqvinop  5436  opcom  5450  fconstmpt  5687  opeliunxp  5692  opeliun2xp  5693  xpundi  5694  elvvv  5701  opelinxp  5705  xpiindi  5785  elcnv2  5827  cnvuni  5836  dmuni  5864  brres  5946  dmres  5972  elidinxp  6004  restidsing  6013  elima3  6027  asymref  6074  imainss  6113  difxp  6123  xpdifid  6127  mptpreima  6197  coundir  6207  resco  6209  coass  6225  relrelss  6232  opreu2reurex  6253  dfpo2  6255  frpoind  6301  ordtri3or  6350  dffun2  6503  dffun6  6504  dffun3  6505  dffun4  6506  dffun5  6507  dffun6f  6508  dffun7  6520  dffun8  6521  dffun9  6522  svrelfun  6565  fncnv  6566  imadif  6577  dfmpt3  6627  fcnvres  6712  fint  6714  fin  6715  dff12  6730  fores  6757  dff1o4  6783  eqfnfv3  6980  fndmin  6992  fniniseg  7007  unpreima  7010  ffnfvf  7067  fsn2  7084  tpres  7150  fconstfv  7161  dff13f  7204  dff14a  7219  dff14b  7220  isocnv2  7280  f1opr  7417  eloprabga  7470  ffnov  7487  eqfnov  7490  foov  7535  uniuni  7710  tfindsg  7806  findsg  7842  funcnvuni  7877  opabex3d  7912  opabex3rd  7913  opabex3  7914  1stconst  8044  2ndconst  8045  frxp  8070  soxp  8073  xpord3lem  8093  suppvalbr  8108  suppofssd  8147  suppcoss  8151  mpoxopovel  8164  brtpos  8179  tpostpos  8190  dfsmo2  8281  dfrecs3  8306  rdglem1  8348  tz7.49  8378  brwitnlem  8436  oeeu  8533  naddasslem2  8625  brinxper  8667  erinxp  8732  mapsncnv  8835  cbvixp  8856  cbvixpv  8857  ixpin  8865  ixpiin  8866  mptelixpg  8877  elixpsn  8879  ixpsnf1o  8880  xpassen  9003  omxpenlem  9010  sbthcl  9031  sbthfilem  9126  wemapsolem  9459  dford2  9535  inf2  9538  zfinf  9554  ttrclselem2  9641  trcl  9643  frind  9668  frr3g  9674  iscard2  9894  leweon  9927  aceq1  10033  dfac3  10037  dfac4  10038  dfac5lem2  10040  dfac5  10045  kmlem3  10069  kmlem4  10070  kmlem14  10080  kmlem15  10081  dfackm  10083  infmap2  10133  fin23lem25  10240  zorn2lem7  10418  brdom6disj  10448  zfcndrep  10531  zfcndinf  10535  fpwwe  10563  axgroth4  10749  grothprim  10751  grothtsk  10752  nqpr  10931  addsrmo  10990  mulsrmo  10991  opelreal  11047  elnnz  12528  elznn0nn  12532  peano2uz2  12611  nnwos  12859  dflt2  13093  xmullem  13210  4fvwrd4  13596  preduz  13598  elfznelfzo  13722  fzind2  13737  fsuppmapnn0fiubex  13948  hashinfxadd  14341  hashgt23el  14380  hashfun  14393  fi1uzind  14463  brfi1uzind  14464  opfi1uzind  14467  cotr2g  14932  shftdm  15027  rexfiuz  15304  cbvsum  15651  cbvsumv  15652  mertenslem2  15844  mertens  15845  cbvprod  15872  cbvprodv  15873  prodeq1i  15875  prodmo  15895  iprodmul  15962  divalglem10  16365  ndvdssub  16372  bitsmod  16399  algcvgblem  16540  isprm2  16645  isprm4  16647  hashdvds  16739  infpn2  16878  hashbc0  16970  xpscf  17523  funcpropd  17863  isffth2  17879  eldmcoa  18026  setcinv  18051  xpccatid  18148  yonedainv  18241  ispos  18274  ispos2  18275  joinfval2  18332  meetfval2  18346  istsr2  18544  isnsg2  19125  isnsg4  19136  isgim  19231  oppgid  19325  oppgcntz  19333  symgfix2  19385  efgval2  19693  iscyg2  19851  dmdprdd  19970  subgdmdprd  20005  issrg  20163  oppr1  20324  opprunit  20351  opprirred  20396  isrnghm  20415  isrhm  20452  issubrng  20518  subsubrng2  20535  subsubrg2  20570  rngcinv  20608  ringcinv  20642  isdomn2  20682  isdomn2OLD  20683  islmim  21052  lbsextg  21155  lidlnz  21235  resubdrg  21601  unocv  21673  pjfval2  21702  islinds2  21806  opsrtoslem1  22046  mdetunilem8  22597  istop2g  22874  isbasis2g  22926  tgval2  22934  isclo2  23066  isnrm2  23336  is1stc2  23420  llyi  23452  isfbas2  23813  elfg  23849  ufinffr  23907  isfcls  23987  alexsubALTlem2  24026  alexsubALTlem3  24027  cnextcn  24045  ustfilxp  24191  iscusp2  24279  metustid  24532  isclmp  25077  iscvsp  25108  tcphcph  25217  iscau3  25258  caucfil  25263  mdegleb  26042  ellogdm  26619  dvdsflsumcom  27168  logfac2  27197  dchrelbas3  27218  dchrvmasumlema  27480  nosupno  27684  noinfno  27699  noinfbnd1lem1  27704  dmcuts  27800  made0  27872  mulsproplem5  28129  norecdiv  28199  elnnzs  28410  uzsind  28414  zsoring  28418  legtrid  28676  outpasch  28840  axcontlem5  29054  axcontlem6  29055  axcontlem7  29056  nb3grpr2  29469  iscplgr  29501  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  32682  unipreima  32734  dfcnv2  32766  1stpreima  32798  isunit2  33319  lsmsnorb2  33470  prmidl0  33528  ssmxidl  33552  1arithufdlem4  33625  ressply1mon1p  33646  extdgfialglem1  33855  zarcls  34037  rhmpreimacnlem  34047  isrnsiga  34276  rossros  34343  omsmeas  34486  eulerpartlemr  34537  eulerpartlemgvv  34539  ballotlemodife  34661  plymulx  34711  signstfvneq0  34735  bnj251  34864  bnj252  34865  bnj257  34869  bnj290  34872  bnj1304  34980  bnj153  35041  bnj543  35054  bnj571  35067  bnj580  35074  bnj607  35077  bnj882  35087  bnj964  35104  bnj996  35117  bnj1033  35130  bnj1176  35166  bnj1186  35168  bnj1189  35170  bnj1204  35173  bnj1253  35178  bnj1452  35213  bnj1463  35216  dff15  35246  axprALT2  35272  fineqvrep  35277  fineqvac  35279  lfuhgr3  35321  cusgredgex2  35324  usgrgt2cycl  35331  2cycl2d  35340  dfacycgr1  35345  erdszelem9  35400  cvmlift2lem9  35512  cvmlift2lem13  35516  satfvsucsuc  35566  satfdm  35570  satf0  35573  fmlasucdisj  35600  satffunlem  35602  satffunlem1lem1  35603  satffunlem2lem1  35605  elmthm  35777  axinfprim  35907  axacprim  35908  xpab  35927  dfso2  35956  dford5reg  35981  dfon2lem5  35986  dfon2  35991  brtxp2  36080  brpprod3a  36085  dfom5b  36111  brcart  36131  brimg  36136  funpartlem  36143  dfrecs2  36151  cgrxfr  36256  segletr  36315  sumeq2si  36403  prodeq2si  36405  cbvprodvw2  36448  trer  36517  fneval  36553  neifg  36572  df3nandALT1  36600  andnand1  36602  nandsym1  36623  weiunlem  36664  regsfromregtco  36739  mh-infprim2bi  36748  mh-infprim3bi  36749  bj-df-sb  36963  bj-dfsbc  36965  bj-eu3f  37167  bj-csbsnlem  37229  bj-snsetex  37289  bj-elsngl  37294  bj-snglc  37295  bj-restuni  37428  bj-dfmpoa  37449  bj-imdirco  37523  mptsnunlem  37671  icorempo  37684  isbasisrelowllem2  37689  relowlpssretop  37697  rdgeqoa  37703  difunieq  37707  dffinxpf  37718  nlpineqsn  37741  curf  37936  finixpnum  37943  ptrest  37957  poimirlem1  37959  poimirlem14  37972  poimirlem16  37974  poimirlem19  37977  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  poimir  37991  cnambfre  38006  itg2addnc  38012  ftc1anc  38039  opropabco  38062  isdrngo1  38294  keridl  38370  ispridlc  38408  selconj  38438  eldmres3  38621  eldmqsres  38631  cnvepres  38642  ecinn0  38691  alrmomorn  38696  moantr  38710  dfxrn2  38723  disjressuc2  38749  inxpxrn  38756  rnxrnres  38760  coss2cnvepres  38846  refrelredund4  39057  dferALTV2  39091  dfeldisj3  39149  dfpart2  39210  dfpeters2  39312  petseq  39314  prtlem70  39320  prtlem100  39322  prtlem15  39338  islshpat  39480  lcvbr2  39485  lcvbr3  39486  lcvnbtwn2  39490  ellkr  39552  cvrval2  39737  cvrnbtwn2  39738  cvrnbtwn3  39739  cvrnbtwn4  39742  ishlat2  39816  lplnexatN  40026  islvol5  40042  dath  40199  pclfinclN  40413  lhpexle3  40475  4atex2  40540  4atex2-0bOLDN  40542  isltrn2N  40583  cdleme0nex  40753  cdleme22b  40804  cdlemg17pq  41135  cdlemg19  41147  cdlemg21  41149  cdlemg33d  41172  dibopelvalN  41606  dibopelval2  41608  dib1dim  41628  dicelval2N  41645  diclspsn  41657  lcdlss  42082  mapd1o  42111  3factsumint2  42478  3factsumint3  42479  3factsumint  42481  hashnexinj  42584  sticksstones16  42618  sticksstones21  42623  unitscyglem3  42653  supinf  42698  fimgmcyclem  42995  eu6w  43126  mzpcompact2lem  43200  fz1eqin  43218  rexrabdioph  43243  expdiophlem1  43470  dford4  43478  fnwe2lem2  43500  fgraphopab  43652  dflim6  43713  onsucf1olem  43719  onsucrn  43720  nnoeomeqom  43761  faosnf0.11b  43875  ifpidg  43939  rp-fakeinunass  43963  rp-isfinite6  43966  dfsucon  43971  elinintrab  44025  elnonrel  44033  elmapintab  44044  dfrtrcl5  44077  imaiun1  44099  coiun1  44100  rfovcnvf1od  44452  andi3or  44472  uneqsn  44473  ntrneicls00  44537  rr-groth  44747  ismnushort  44749  rr-grothshortbi  44751  2sbc5g  44864  pm14.12  44869  2sb5nd  45008  uun2221  45260  uun2221p1  45261  uun2221p2  45262  2sb5ndVD  45357  2sb5ndALT  45379  modelaxreplem3  45428  iindif2f  45611  disjinfi  45643  climuz  46193  dfxlim2  46297  cncfshift  46323  dvnmul  46392  dvnprodlem2  46396  ismbl3  46435  ismbl4  46442  stoweidlem26  46475  stoweidlem35  46484  fourierdlem54  46609  fourierdlem83  46638  fourierdlem100  46655  fourierdlem104  46659  fourierdlem109  46664  fourierdlem112  46667  smfpimcc  47257  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