Theorem anbi2i 635

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1ci  638  anbi12i  640  bianass  655  an42  670  anandir  690  dfbi3  1065  dn1  1073  dfifp3  1081  ifpdfbiOLD  1087  4anpull2OLD  1383  an3andi  1513  an33rean  1514  anxordi  1555  cadcoma  1644  nic-mpALT  1704  nic-axALT  1706  3exdistr  1994  4exdistr  1995  19.27v  2029  19.27  2266  19.41  2274  2sb5  2314  dfsb7  2315  dfeumo  2564  mo4f  2595  eu3v  2598  eu6  2602  dfeu  2623  eu2  2637  eu4  2643  2mos  2677  2eu4  2682  r3ex  3204  ceqsex3v  3505  ceqsex4v  3506  ceqsex8v  3508  reu2  3685  reu6  3686  reu4  3691  reu7  3692  rmo3f  3694  rmo4f  3695  2reu5lem3  3717  2reu5  3718  sbcimdv  3809  sbcg  3813  rmo3  3839  reuan  3847  dfpss2  4017  difdif  4073  raldifb  4087  inass  4126  dfss4  4216  dfin2  4218  indi  4231  indifdi  4241  undif3  4247  difin0ss  4323  inssdif0OLD  4325  2nreu  4404  2reu4lem  4481  rexdifpr  4619  reuprg0  4662  ssdifsn  4750  ssunpr  4791  uniprg  4885  uniun  4892  uniinOLD  4894  csbuni  4900  dfiun2g  4990  iunin2  5031  iundif2  5034  iindif2  5039  iinin2  5040  elpwpw  5064  axrep1  5235  axrep4v  5239  axrep4  5240  reusv2lem4  5366  eqvinop  5459  eqvinot  5460  opcom  5476  fconstmpt  5716  opeliunxp  5721  opeliun2xp  5722  xpundi  5723  elvvv  5731  opelinxp  5735  xpiindi  5816  elcnv2  5859  cnvuni  5872  dmuni  5900  brres  5981  dmres  6008  elidinxp  6041  restidsing  6050  elima3  6068  asymref  6115  imainss  6149  difxp  6160  xpdifid  6164  xpdifcnvepel  6165  mptpreima  6245  coundir  6255  resco  6257  coass  6273  relrelss  6281  opreu2reurex  6303  dfpo2  6305  frpoind  6351  ordtri3or  6401  dffun2  6556  dffun6  6557  dffun3  6558  dffun4  6559  dffun5  6560  dffun6f  6561  dffun7  6575  dffun8  6576  dffun9  6577  svrelfun  6620  fncnv  6621  imadif  6632  dfmpt3  6681  fcnvres  6767  fint  6769  fin  6770  dff12  6785  fores  6814  dff1o4  6841  eqfnfv3  7039  fndmin  7052  fniniseg  7067  unpreima  7070  ffnfvf  7128  fsn2  7145  tpres  7214  fconstfv  7225  dff13f  7266  dff14a  7281  dff14b  7282  dff15  7283  isocnv2  7346  f1opr  7483  eloprabga  7536  ffnov  7553  eqfnov  7556  foov  7602  uniuni  7783  tfindsg  7879  findsg  7916  funcnvuni  7951  opabex3d  7984  opabex3rd  7985  opabex3  7986  1stconst  8121  2ndconst  8122  frxp  8148  soxp  8151  fnwe2lem3  8157  xpord3lem  8176  suppvalbrOLD  8192  suppofssd  8231  suppcoss  8235  mpoxopovel  8248  brtpos  8263  tpostpos  8274  dfsmo2  8366  dfrecs3  8391  rdglem1  8434  tz7.49  8466  brwitnlem  8526  oeeu  8623  naddasslem2  8716  brinxper  8758  erinxp  8823  curf  8901  mapsncnv  8932  cbvixp  8953  cbvixpv  8954  ixpin  8962  ixpiin  8963  mptelixpg  8974  elixpsn  8976  ixpsnf1o  8977  xpassen  9101  omxpenlem  9108  sbthcl  9129  sbthfilem  9224  wemapsolem  9554  dford2  9631  inf2  9634  zfinf  9650  ttrclselem2  9737  trcl  9739  frind  9764  frr3g  9770  elhf3  9923  setrec1lem3  9979  dffun3f  9985  iscard2  10067  leweon  10100  aceq1  10206  dfac3  10210  dfac4  10211  dfac5lem2  10213  dfac5  10217  kmlem3  10241  kmlem4  10242  kmlem14  10252  kmlem15  10253  dfackm  10255  infmap2  10305  fin23lem25  10412  zorn2lem7  10590  brdom6disj  10621  zfcndrep  10709  zfcndinf  10713  fpwwe  10741  axgroth4  10927  grothprim  10929  grothtsk  10930  nqpr  11109  addsrmo  11168  mulsrmo  11169  opelreal  11225  elnnz  12713  elznn0nn  12717  peano2uz2  12797  nnwos  13052  dflt2  13287  xmullem  13404  4fvwrd4  13792  preduz  13794  elfznelfzo  13918  fzind2  13933  fsuppmapnn0fiubex  14145  hashinfxadd  14539  hashgt23el  14579  hashfun  14592  fi1uzind  14662  brfi1uzind  14663  opfi1uzind  14666  cotr2g  15141  shftdm  15236  rexfiuz  15527  cbvsum  15874  cbvsumv  15875  mertenslem2  16066  mertens  16067  cbvprod  16094  cbvprodv  16095  prodeq1i  16097  prodmo  16115  iprodmul  16182  divalglem10  16584  ndvdssub  16591  bitsmod  16618  algcvgblem  16764  isprm2  16869  isprm4  16871  hashdvds  16964  infpn2  17103  hashbc0  17195  xpscf  17749  funcpropd  18089  isffth2  18105  eldmcoa  18252  setcinv  18277  xpccatid  18374  yonedainv  18467  ispos  18500  ispos2  18501  joinfval2  18558  meetfval2  18572  istsr2  18770  isnsg2  19378  isnsg4  19389  isgim  19488  oppgid  19582  oppgcntz  19590  symgfix2  19642  efgval2  19950  iscyg2  20108  dmdprdd  20227  subgdmdprd  20262  issrg  20426  dfring3  20530  oppr1  20592  opprunit  20619  opprirred  20664  isrnghm  20683  isrhm  20721  dfric2  20769  issubrng  20811  subsubrng2  20828  subsubrg2  20863  rngcinv  20901  ringcinv  20935  isdomn2  20975  islmim  21349  lbsextg  21452  lidlnz  21542  prmidl0  21646  resubdrg  21926  unocv  21998  pjfval2  22027  islinds2  22131  opsrtoslem1  22376  mdetunilem8  22946  istop2g  23226  isbasis2g  23278  tgval2  23286  isclo2  23418  isnrm2  23688  is1stc2  23772  llyi  23805  isfbas2  24166  elfg  24202  ufinffr  24260  isfcls  24340  alexsubALTlem2  24379  alexsubALTlem3  24380  cnextcn  24398  ustfilxp  24544  iscusp2  24632  metustid  24885  isclmp  25430  iscvsp  25461  tcphcph  25570  iscau3  25611  caucfil  25616  mdegleb  26394  plymulidp  26615  ellogdm  26979  dvdsflsumcom  27527  logfac2  27556  dchrelbas3  27577  dchrvmasumlema  27839  nosupno  28072  noinfno  28087  noinfbnd1lem1  28092  dmcuts  28189  made0  28261  mulsproplem5  28518  norecdiv  28588  elnnzs  28799  uzsind  28803  zsoring  28807  legtrid  29066  outpasch  29245  tgaaddcpbllem2  29362  tgaaddcpbllem3  29363  tgaltai  29457  axcontlem5  29558  axcontlem6  29559  axcontlem7  29560  lfuhgr3  29740  nb3grpr2  29976  iscplgr  30008  dfpth2  30326  pthdlem1  30364  wwlksnextinj  30500  usgr2wspthon  30569  rusgrnumwwlkl1  30572  isclwwlk  30587  clwwlkccatlem  30592  clwwlknon2x  30706  dfacycgr1  30762  iseupthf1o  30815  frcond3  30882  frgr3v  30888  4cycl2vnunb  30903  frgrncvvdeqlem2  30913  fusgr2wsp2nb  30947  numclwlk1lem1  30982  hhcms  31817  isch3  31855  ocsh  31897  pjhtheu  32008  pjpreeq  32012  h1deoi  32163  h1dei  32164  eleigvec  32571  cvbr2  32897  cvnbtwn2  32901  cvnbtwn4  32903  mdsl2i  32936  cvmdi  32938  mdsymlem6  33022  cdj3lem3b  33054  mo5f  33139  nmo  33140  rexunirn  33142  dmrab  33147  difrab2  33148  disjunsn  33242  unipreima  33291  dfcnv2  33323  1stpreima  33354  isunit2  33853  lsmsnorb2  34000  ssmxidl  34052  1arithufdlem4  34132  ressply1mon1p  34153  extdgfialglem1  34377  zarcls  34559  rhmpreimacnlem  34569  isrnsiga  34798  rossros  34866  omsmeas  35008  eulerpartlemr  35059  eulerpartlemgvv  35061  ballotlemodife  35183  signstfvneq0  35254  bnj251  35386  bnj252  35387  bnj257  35391  bnj290  35394  bnj1304  35502  bnj153  35563  bnj543  35576  bnj571  35589  bnj580  35596  bnj607  35599  bnj882  35609  bnj964  35626  bnj996  35639  bnj1033  35652  bnj1176  35688  bnj1186  35690  bnj1189  35692  bnj1204  35695  bnj1253  35700  bnj1452  35735  bnj1463  35738  reu6f  35762  r1omhf  35792  axprALT2  35795  fineqvrep  35853  fineqvac  35855  kardexen  35902  onprcf1acwevdlem1  35999  cusgredgex2  36018  usgrgt2cycl  36020  2cycl2d  36023  erdszelem9  36085  cvmlift2lem9  36197  cvmlift2lem13  36201  satfvsucsuc  36251  satfdm  36255  satf0  36258  fmlasucdisj  36285  satffunlem  36287  satffunlem1lem1  36288  satffunlem2lem1  36290  elmthm  36462  axinfprim  36598  axacprim  36599  xpab  36618  dfso2  36647  dford5reg  36671  dfon2lem5  36676  dfon2  36681  brtxp2  36770  brpprod3a  36775  dfom5b  36801  brcart  36821  brimg  36826  funpartlem  36833  dfrecs2  36841  cgrxfr  36947  segletr  37006  sumeq2si  37118  prodeq2si  37120  cbvprodvw2  37163  trer  37231  fneval  37267  neifg  37286  df3nandALT1  37314  andnand1  37316  nandsym1  37337  weiunlem  37378  regsfromregtco  37453  mh-infprim2bi  37462  mh-infprim3bi  37463  bj-df-sb  37676  bj-dfsbc  37678  bj-eu3f  37880  bj-csbsnlem  37942  bj-snsetex  38003  bj-elsngl  38008  bj-snglc  38009  bj-elinxp  38087  bj-restuni  38157  bj-dfmpoa  38179  bj-imdirco  38251  mptsnunlem  38401  icorempo  38414  isbasisrelowllem2  38419  relowlpssretop  38427  rdgeqoa  38433  difunieq  38437  dffinxpf  38448  nlpineqsn  38471  finixpnum  38668  ptrest  38677  poimirlem1  38679  poimirlem14  38692  poimirlem16  38694  poimirlem19  38697  poimirlem25  38703  poimirlem26  38704  poimirlem27  38705  poimir  38711  cnambfre  38726  itg2addnc  38732  ftc1anc  38759  dfprop1  38785  opropabco  38798  isdrngo1  39030  keridl  39106  ispridlc  39144  selconj  39172  eldmres3  39355  eldmqsres  39365  cnvepres  39376  ecinn0  39425  alrmomorn  39430  moantr  39444  dfxrn2  39457  disjressuc2  39483  inxpxrn  39490  rnxrnres  39494  coss2cnvepres  39580  refrelredund4  39791  dferALTV2  39825  dfeldisj3  39883  dfpart2  39944  dfpeters2  40046  petseq  40048  prtlem70  40054  prtlem100  40056  prtlem15  40072  islshpat  40214  lcvbr2  40219  lcvbr3  40220  lcvnbtwn2  40224  ellkr  40286  cvrval2  40471  cvrnbtwn2  40472  cvrnbtwn3  40473  cvrnbtwn4  40476  ishlat2  40550  lplnexatN  40760  islvol5  40776  dath  40933  pclfinclN  41147  lhpexle3  41209  4atex2  41274  4atex2-0bOLDN  41276  isltrn2N  41317  cdleme0nex  41487  cdleme22b  41538  cdlemg17pq  41869  cdlemg19  41881  cdlemg21  41883  cdlemg33d  41906  dibopelvalN  42340  dibopelval2  42342  dib1dim  42362  dicelval2N  42379  diclspsn  42391  lcdlss  42816  mapd1o  42845  3factsumint2  43212  3factsumint3  43213  3factsumint  43215  hashnexinj  43318  sticksstones16  43352  sticksstones21  43357  unitscyglem3  43387  supinf  43433  fimgmcyclem  43737  eu6w  43827  mzpcompact2lem  43902  fz1eqin  43920  rexrabdioph  43941  expdiophlem1  44168  dford4  44176  fgraphopab  44345  dflim6  44406  onsucf1olem  44412  onsucrn  44413  nnoeomeqom  44454  faosnf0.11b  44568  ifpidg  44632  rp-fakeinunass  44656  rp-isfinite6  44659  dfsucon  44664  elinintrab  44718  elnonrel  44726  elmapintab  44736  dfrtrcl5  44769  imaiun1  44791  coiun1  44792  rfovcnvf1od  45144  andi3or  45164  uneqsn  45165  ntrneicls00  45229  rr-groth  45423  ismnushort  45425  rr-grothshortbi  45427  2sbc5g  45540  pm14.12  45544  2sb5nd  45682  uun2221  45934  uun2221p1  45935  uun2221p2  45936  2sb5ndVD  46031  2sb5ndALT  46053  modelaxreplem3  46109  iindif2f  46314  disjinfi  46346  climuz  46893  dfxlim2  46997  cncfshift  47023  dvnmul  47092  dvnprodlem2  47096  ismbl3  47135  ismbl4  47142  stoweidlem26  47175  stoweidlem35  47184  fourierdlem54  47309  fourierdlem83  47338  fourierdlem100  47355  fourierdlem104  47359  fourierdlem109  47364  fourierdlem112  47367  smfpimcc  47957  fcoresf1ob  48282  f1cof1b  48286  f1ocof1ob  48290  2reu8i  48323  dfdfat2  48337  ffnaov  48408  an4com24  48477  4an21  48479  iccpartiltu  48643  prproropf1olem0  48723  dfgric2  49152  gpgvtxedg0  49300  gpgvtxedg1  49301  gpgprismgr4cycllem10  49341  grlimedgnedg  49368  2zrngmmgm  49488  rngcinvALTV  49512  ringcinvALTV  49546  isprmrng  49572  pgrpgt2nabl  49617  islindeps  49704  lindslinindsimp1  49708  lindslinindsimp2  49714  ldepslinc  49760  blen1b  49839  rrx2xpref1o  49970  coxp  50083  i0oii  50173  io1ii  50174  isthinc2  50694  isthinc3  50695  isthincd2  50711  istermc2  50749  istermc3  50750  parhomel  50883  elpglem3  51020  elpg  51021  alsanmo  51120  ralsanmo  51121  2alsraln0  51127  2alsraln0id  51128