Theorem anbi2i 622

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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi1ci  625  anbi12i  627  bianass  641  an42  656  anandir  676  dfbi3  1048  dn1  1056  dfifp3  1064  ifpdfbi  1069  an3andi  1479  an33rean  1480  anxordi  1520  cadcoma  1606  nic-mpALT  1667  nic-axALT  1669  3exdistr  1957  4exdistr  1958  19.27v  1986  19.27  2216  19.41  2224  2sb5  2267  dfsb7  2269  dfeumo  2527  mo4f  2557  eu3v  2560  eu6  2564  dfeu  2585  eu2  2601  eu4  2607  2mos  2641  2eu4  2646  ceqsex3v  3528  ceqsex4v  3529  ceqsex8v  3531  reu2  3719  reu6  3720  reu4  3725  reu7  3726  rmo3f  3728  rmo4f  3729  2reu5lem3  3751  2reu5  3752  sbcimdv  3848  sbcg  3853  rmo3  3880  reuan  3887  dfpss2  4082  difdif  4127  raldifb  4141  inass  4216  dfss4  4255  dfin2  4257  indi  4270  indifdi  4280  indifdirOLD  4282  undif3  4287  difin0ss  4365  inssdif0  4366  2nreu  4438  2reu4lem  4522  rexdifpr  4658  reuprg0  4703  ssdifsn  4788  ssunpr  4832  uniprg  4920  uniprOLD  4922  uniun  4929  uniin  4930  csbuni  4935  dfiun2g  5028  iunin2  5069  iundif2  5072  iindif2  5075  iinin2  5076  elpwpw  5100  axrep1  5281  axrep4  5285  reusv2lem4  5396  eqvinop  5484  opcom  5498  fconstmpt  5735  opeliunxp  5740  xpundi  5741  elvvv  5748  opelinxp  5752  xpiindi  5833  elcnv2  5875  cnvuni  5884  dmuni  5912  brres  5987  dmres  6002  elidinxp  6042  restidsing  6051  elima3  6065  asymref  6117  imainss  6153  difxp  6163  xpdifid  6167  mptpreima  6237  coundir  6247  resco  6249  coass  6264  relrelss  6272  opreu2reurex  6293  dfpo2  6295  frpoind  6343  wfiOLD  6352  ordtri3or  6396  dffun2  6553  dffun2OLD  6554  dffun2OLDOLD  6555  dffun6  6556  dffun3  6557  dffun3OLD  6558  dffun4  6559  dffun5  6560  dffun6f  6561  dffun7  6575  dffun8  6576  dffun9  6577  svrelfun  6620  fncnv  6621  imadif  6632  dfmpt3  6684  fcnvres  6769  fint  6771  fin  6772  dff12  6787  fores  6816  dff1o4  6842  eqfnfv3  7037  fndmin  7049  fniniseg  7064  unpreima  7067  ffnfvf  7125  fsn2  7140  tpres  7208  fconstfv  7219  dff13f  7261  dff14a  7275  dff14b  7276  isocnv2  7334  f1opr  7471  eloprabga  7523  ffnov  7542  eqfnov  7545  foov  7590  uniuni  7759  tfindsg  7860  findsg  7900  funcnvuni  7934  opabex3d  7964  opabex3rd  7965  opabex3  7966  1stconst  8100  2ndconst  8101  frxp  8126  soxp  8129  xpord3lem  8149  suppvalbr  8164  suppofssd  8203  suppcoss  8207  mpoxopovel  8220  brtpos  8235  tpostpos  8246  dfsmo2  8362  dfrecs3  8387  dfrecs3OLD  8388  rdglem1  8430  tz7.49  8460  brwitnlem  8522  oeeu  8618  naddasslem2  8710  erinxp  8804  mapsncnv  8906  cbvixp  8927  ixpin  8936  ixpiin  8937  mptelixpg  8948  elixpsn  8950  ixpsnf1o  8951  xpassen  9085  omxpenlem  9092  sbthcl  9114  sbthfilem  9220  wemapsolem  9568  dford2  9638  inf2  9641  zfinf  9657  ttrclselem2  9744  trcl  9746  frind  9768  frr3g  9774  iscard2  9994  leweon  10029  aceq1  10135  dfac3  10139  dfac4  10140  dfac5lem2  10142  dfac5  10146  kmlem3  10170  kmlem4  10171  kmlem14  10181  kmlem15  10182  dfackm  10184  infmap2  10236  fin23lem25  10342  zorn2lem7  10520  brdom6disj  10550  zfcndrep  10632  zfcndinf  10636  fpwwe  10664  axgroth4  10850  grothprim  10852  grothtsk  10853  nqpr  11032  addsrmo  11091  mulsrmo  11092  opelreal  11148  elnnz  12593  elznn0nn  12597  peano2uz2  12675  nnwos  12924  dflt2  13154  xmullem  13270  4fvwrd4  13648  preduz  13650  elfznelfzo  13764  fzind2  13777  fsuppmapnn0fiubex  13984  hashinfxadd  14371  hashgt23el  14410  hashfun  14423  fi1uzind  14485  brfi1uzind  14486  opfi1uzind  14489  cotr2g  14950  shftdm  15045  rexfiuz  15321  cbvsum  15668  mertenslem2  15858  mertens  15859  cbvprod  15886  prodmo  15907  iprodmul  15974  divalglem10  16373  ndvdssub  16380  bitsmod  16405  algcvgblem  16542  isprm2  16647  isprm4  16649  hashdvds  16738  infpn2  16876  hashbc0  16968  xpscf  17541  funcpropd  17883  isffth2  17899  eldmcoa  18048  setcinv  18073  xpccatid  18173  yonedainv  18267  ispos  18300  ispos2  18301  joinfval2  18360  meetfval2  18374  istsr2  18570  isnsg2  19105  isnsg4  19116  isgim  19210  oppgid  19304  oppgcntz  19312  symgfix2  19365  efgval2  19673  iscyg2  19831  dmdprdd  19950  subgdmdprd  19985  issrg  20122  oppr1  20283  opprunit  20310  opprirred  20355  isrnghm  20374  isrhm  20411  issubrng  20478  subsubrng2  20495  subsubrg2  20532  rngcinv  20564  ringcinv  20598  islmim  20941  lbsextg  21044  lidlnz  21131  isdomn2  21240  resubdrg  21534  unocv  21606  pjfval2  21637  islinds2  21741  opsrtoslem1  21993  mdetunilem8  22515  istop2g  22792  isbasis2g  22845  tgval2  22853  isclo2  22986  isnrm2  23256  is1stc2  23340  llyi  23372  isfbas2  23733  elfg  23769  ufinffr  23827  isfcls  23907  alexsubALTlem2  23946  alexsubALTlem3  23947  cnextcn  23965  ustfilxp  24111  iscusp2  24201  metustid  24457  isclmp  25018  iscvsp  25049  tcphcph  25159  iscau3  25200  caucfil  25205  mdegleb  25994  ellogdm  26567  dvdsflsumcom  27114  logfac2  27144  dchrelbas3  27165  dchrvmasumlema  27427  nosupno  27630  noinfno  27645  noinfbnd1lem1  27650  dmscut  27738  made0  27794  mulsproplem5  28014  norecdiv  28084  legtrid  28389  outpasch  28553  axcontlem5  28773  axcontlem6  28774  axcontlem7  28775  nb3grpr2  29190  iscplgr  29222  pthdlem1  29574  wwlksnextinj  29704  usgr2wspthon  29770  rusgrnumwwlkl1  29773  isclwwlk  29788  clwwlkccatlem  29793  clwwlknon2x  29907  iseupthf1o  30006  frcond3  30073  frgr3v  30079  4cycl2vnunb  30094  frgrncvvdeqlem2  30104  fusgr2wsp2nb  30138  numclwlk1lem1  30173  hhcms  31007  isch3  31045  ocsh  31087  pjhtheu  31198  pjpreeq  31202  h1deoi  31353  h1dei  31354  eleigvec  31761  cvbr2  32087  cvnbtwn2  32091  cvnbtwn4  32093  mdsl2i  32126  cvmdi  32128  mdsymlem6  32212  cdj3lem3b  32244  mo5f  32281  nmo  32282  rexunirn  32284  dmrab  32289  difrab2  32290  disjunsn  32378  unipreima  32424  dfcnv2  32456  1stpreima  32481  lsmsnorb2  33096  prmidl0  33161  ssmxidl  33182  ressply1mon1p  33238  zarcls  33470  rhmpreimacnlem  33480  isrnsiga  33727  rossros  33794  omsmeas  33938  eulerpartlemr  33989  eulerpartlemgvv  33991  ballotlemodife  34112  plymulx  34175  signstfvneq0  34199  bnj251  34328  bnj252  34329  bnj257  34333  bnj290  34336  bnj1304  34445  bnj153  34506  bnj543  34519  bnj571  34532  bnj580  34539  bnj607  34542  bnj882  34552  bnj964  34569  bnj996  34582  bnj1033  34595  bnj1176  34631  bnj1186  34633  bnj1189  34635  bnj1204  34638  bnj1253  34643  bnj1452  34678  bnj1463  34681  dff15  34702  fineqvrep  34710  fineqvac  34712  lfuhgr3  34724  cusgredgex2  34727  usgrgt2cycl  34735  2cycl2d  34744  dfacycgr1  34749  erdszelem9  34804  cvmlift2lem9  34916  cvmlift2lem13  34920  satfvsucsuc  34970  satfdm  34974  satf0  34977  fmlasucdisj  35004  satffunlem  35006  satffunlem1lem1  35007  satffunlem2lem1  35009  elmthm  35181  axinfprim  35295  axacprim  35296  xpab  35315  dfso2  35344  dford5reg  35373  dfon2lem5  35378  dfon2  35383  brtxp2  35472  brpprod3a  35477  dfom5b  35503  brcart  35523  brimg  35528  funpartlem  35533  dfrecs2  35541  cgrxfr  35646  segletr  35705  trer  35795  fneval  35831  neifg  35850  df3nandALT1  35878  andnand1  35880  nandsym1  35901  bj-eu3f  36313  bj-csbsnlem  36376  bj-snsetex  36437  bj-elsngl  36442  bj-snglc  36443  bj-restuni  36571  bj-dfmpoa  36592  bj-imdirco  36664  mptsnunlem  36812  icorempo  36825  isbasisrelowllem2  36830  relowlpssretop  36838  rdgeqoa  36844  difunieq  36848  dffinxpf  36859  nlpineqsn  36882  curf  37066  finixpnum  37073  ptrest  37087  poimirlem1  37089  poimirlem14  37102  poimirlem16  37104  poimirlem19  37107  poimirlem25  37113  poimirlem26  37114  poimirlem27  37115  poimir  37121  cnambfre  37136  itg2addnc  37142  ftc1anc  37169  opropabco  37192  isdrngo1  37424  keridl  37500  ispridlc  37538  selconj  37568  eldmqsres  37754  cnvepres  37765  ecinn0  37820  alrmomorn  37825  moantr  37831  dfxrn2  37843  disjressuc2  37855  inxpxrn  37862  rnxrnres  37866  coss2cnvepres  37885  refrelredund4  38102  dferALTV2  38135  dfeldisj3  38186  dfpart2  38236  prtlem70  38324  prtlem100  38326  prtlem15  38342  islshpat  38484  lcvbr2  38489  lcvbr3  38490  lcvnbtwn2  38494  ellkr  38556  cvrval2  38741  cvrnbtwn2  38742  cvrnbtwn3  38743  cvrnbtwn4  38746  ishlat2  38820  lplnexatN  39031  islvol5  39047  dath  39204  pclfinclN  39418  lhpexle3  39480  4atex2  39545  4atex2-0bOLDN  39547  isltrn2N  39588  cdleme0nex  39758  cdleme22b  39809  cdlemg17pq  40140  cdlemg19  40152  cdlemg21  40154  cdlemg33d  40177  dibopelvalN  40611  dibopelval2  40613  dib1dim  40633  dicelval2N  40650  diclspsn  40662  lcdlss  41087  mapd1o  41116  3factsumint2  41488  3factsumint3  41489  3factsumint  41491  hashnexinj  41594  sticksstones16  41629  sticksstones21  41634  metakunt1  41648  mzpcompact2lem  42162  fz1eqin  42180  rexrabdioph  42205  expdiophlem1  42433  dford4  42441  fnwe2lem2  42466  fgraphopab  42622  dflim6  42684  onsucf1olem  42690  onsucrn  42691  nnoeomeqom  42732  faosnf0.11b  42848  ifpidg  42912  rp-fakeinunass  42936  rp-isfinite6  42939  dfsucon  42944  elinintrab  42998  elnonrel  43006  elmapintab  43017  dfrtrcl5  43050  imaiun1  43072  coiun1  43073  rfovcnvf1od  43425  andi3or  43445  uneqsn  43446  ntrneicls00  43510  rr-groth  43727  ismnushort  43729  rr-grothshortbi  43731  2sbc5g  43844  pm14.12  43849  2sb5nd  43990  uun2221  44243  uun2221p1  44244  uun2221p2  44245  2sb5ndVD  44340  2sb5ndALT  44362  iindif2f  44522  disjinfi  44556  climuz  45123  dfxlim2  45227  cncfshift  45253  dvnmul  45322  dvnprodlem2  45326  ismbl3  45365  ismbl4  45372  stoweidlem26  45405  stoweidlem35  45414  fourierdlem54  45539  fourierdlem83  45568  fourierdlem100  45585  fourierdlem104  45589  fourierdlem109  45594  fourierdlem112  45597  smfpimcc  46187  fcoresf1ob  46446  f1cof1b  46448  f1ocof1ob  46452  2reu8i  46484  dfdfat2  46499  ffnaov  46570  an4com24  46639  4an21  46641  iccpartiltu  46753  prproropf1olem0  46833  dfgric2  47172  2zrngmmgm  47305  rngcinvALTV  47329  ringcinvALTV  47363  opeliun2xp  47387  pgrpgt2nabl  47421  islindeps  47512  lindslinindsimp1  47516  lindslinindsimp2  47522  ldepslinc  47568  blen1b  47652  i0oii  47929  io1ii  47930  iscnrm3lem3  47945  isthinc2  48019  isthinc3  48020  isthincd2  48035  dffun3f  48104  setrec1lem3  48111  elpglem3  48135  elpg  48136