Theorem anbi2i 632

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi1ci  635  anbi12i  637  bianass  652  an42  667  anandir  687  dfbi3  1061  dn1  1069  dfifp3  1077  ifpdfbi  1082  4anpull2  1375  an3andi  1503  an33rean  1504  anxordi  1546  cadcoma  1632  nic-mpALT  1692  nic-axALT  1694  3exdistr  1980  4exdistr  1981  19.27v  2015  19.27  2262  19.41  2270  2sb5  2312  dfsb7  2313  dfeumo  2563  mo4f  2594  eu3v  2597  eu6  2601  dfeu  2622  eu2  2636  eu4  2642  2mos  2676  2eu4  2681  r3ex  3201  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  reu2  3688  reu6  3689  reu4  3694  reu7  3695  rmo3f  3697  rmo4f  3698  2reu5lem3  3720  2reu5  3721  sbcimdv  3812  sbcg  3816  rmo3  3842  reuan  3849  dfpss2  4041  difdif  4088  raldifb  4102  inass  4179  dfss4  4221  dfin2  4223  indi  4236  indifdi  4246  undif3  4252  difin0ss  4326  inssdif0  4327  2nreu  4398  2reu4lem  4477  rexdifpr  4618  reuprg0  4661  ssdifsn  4748  ssunpr  4792  uniprg  4881  uniun  4888  uniinOLD  4890  csbuni  4896  dfiun2g  4987  iunin2  5028  iundif2  5031  iindif2  5034  iinin2  5035  elpwpw  5059  axrep1  5228  axrep4v  5232  axrep4  5233  axrep4OLD  5234  reusv2lem4  5358  eqvinop  5455  opcom  5470  fconstmpt  5709  opeliunxp  5714  opeliun2xp  5715  xpundi  5716  elvvv  5723  opelinxp  5727  xpiindi  5807  elcnv2  5849  cnvuni  5862  dmuni  5890  brres  5972  dmres  5998  elidinxp  6033  restidsing  6042  elima3  6056  asymref  6103  imainss  6139  difxp  6149  xpdifid  6153  xpdifcnvepel  6154  mptpreima  6225  coundir  6235  resco  6237  coass  6253  relrelss  6260  opreu2reurex  6281  dfpo2  6283  frpoind  6329  ordtri3or  6378  dffun2  6531  dffun6  6532  dffun3  6533  dffun4  6534  dffun5  6535  dffun6f  6536  dffun7  6548  dffun8  6549  dffun9  6550  svrelfun  6593  fncnv  6594  imadif  6605  dfmpt3  6655  fcnvres  6741  fint  6743  fin  6744  dff12  6759  fores  6788  dff1o4  6815  eqfnfv3  7013  fndmin  7026  fniniseg  7041  unpreima  7044  ffnfvf  7101  fsn2  7118  tpres  7185  fconstfv  7196  dff13f  7239  dff14a  7254  dff14b  7255  isocnv2  7315  f1opr  7452  eloprabga  7505  ffnov  7522  eqfnov  7525  foov  7570  uniuni  7745  tfindsg  7841  findsg  7878  funcnvuni  7913  opabex3d  7946  opabex3rd  7947  opabex3  7948  1stconst  8079  2ndconst  8080  frxp  8106  soxp  8109  xpord3lem  8129  suppvalbr  8144  suppofssd  8183  suppcoss  8187  mpoxopovel  8200  brtpos  8215  tpostpos  8226  dfsmo2  8318  dfrecs3  8343  rdglem1  8386  tz7.49  8416  brwitnlem  8476  oeeu  8573  naddasslem2  8666  brinxper  8708  erinxp  8773  mapsncnv  8875  cbvixp  8896  cbvixpv  8897  ixpin  8905  ixpiin  8906  mptelixpg  8917  elixpsn  8919  ixpsnf1o  8920  xpassen  9043  omxpenlem  9050  sbthcl  9071  sbthfilem  9166  wemapsolem  9498  dford2  9575  inf2  9578  zfinf  9594  ttrclselem2  9681  trcl  9683  frind  9708  frr3g  9714  iscard2  9934  leweon  9967  aceq1  10073  dfac3  10077  dfac4  10078  dfac5lem2  10080  dfac5  10085  kmlem3  10109  kmlem4  10110  kmlem14  10120  kmlem15  10121  dfackm  10123  infmap2  10173  fin23lem25  10281  zorn2lem7  10459  brdom6disj  10489  zfcndrep  10572  zfcndinf  10576  fpwwe  10604  axgroth4  10790  grothprim  10792  grothtsk  10793  nqpr  10972  addsrmo  11031  mulsrmo  11032  opelreal  11088  elnnz  12578  elznn0nn  12582  peano2uz2  12661  nnwos  12916  dflt2  13150  xmullem  13267  4fvwrd4  13653  preduz  13655  elfznelfzo  13779  fzind2  13794  fsuppmapnn0fiubex  14005  hashinfxadd  14398  hashgt23el  14437  hashfun  14450  fi1uzind  14520  brfi1uzind  14521  opfi1uzind  14524  cotr2g  14989  shftdm  15084  rexfiuz  15375  cbvsum  15722  cbvsumv  15723  mertenslem2  15915  mertens  15916  cbvprod  15943  cbvprodv  15944  prodeq1i  15946  prodmo  15966  iprodmul  16033  divalglem10  16436  ndvdssub  16443  bitsmod  16470  algcvgblem  16611  isprm2  16716  isprm4  16718  hashdvds  16810  infpn2  16949  hashbc0  17041  xpscf  17595  funcpropd  17935  isffth2  17951  eldmcoa  18098  setcinv  18123  xpccatid  18220  yonedainv  18313  ispos  18346  ispos2  18347  joinfval2  18404  meetfval2  18418  istsr2  18616  isnsg2  19197  isnsg4  19208  isgim  19302  oppgid  19396  oppgcntz  19404  symgfix2  19456  efgval2  19764  iscyg2  19922  dmdprdd  20041  subgdmdprd  20076  issrg  20238  oppr1  20399  opprunit  20426  opprirred  20471  isrnghm  20490  isrhm  20527  issubrng  20597  subsubrng2  20614  subsubrg2  20649  rngcinv  20687  ringcinv  20721  isdomn2  20761  isdomn2OLD  20762  islmim  21129  lbsextg  21232  lidlnz  21312  resubdrg  21660  unocv  21732  pjfval2  21761  islinds2  21865  opsrtoslem1  22108  mdetunilem8  22679  istop2g  22956  isbasis2g  23008  tgval2  23016  isclo2  23148  isnrm2  23418  is1stc2  23502  llyi  23534  isfbas2  23895  elfg  23931  ufinffr  23989  isfcls  24069  alexsubALTlem2  24108  alexsubALTlem3  24109  cnextcn  24127  ustfilxp  24273  iscusp2  24361  metustid  24614  isclmp  25159  iscvsp  25190  tcphcph  25299  iscau3  25340  caucfil  25345  mdegleb  26124  plymulidp  26346  ellogdm  26704  dvdsflsumcom  27252  logfac2  27281  dchrelbas3  27302  dchrvmasumlema  27564  nosupno  27767  noinfno  27782  noinfbnd1lem1  27787  dmcuts  27884  made0  27956  mulsproplem5  28213  norecdiv  28283  elnnzs  28494  uzsind  28498  zsoring  28502  legtrid  28760  outpasch  28928  axcontlem5  29169  axcontlem6  29170  axcontlem7  29171  nb3grpr2  29584  iscplgr  29616  dfpth2  29929  pthdlem1  29966  wwlksnextinj  30099  usgr2wspthon  30168  rusgrnumwwlkl1  30171  isclwwlk  30186  clwwlkccatlem  30191  clwwlknon2x  30305  iseupthf1o  30404  frcond3  30471  frgr3v  30477  4cycl2vnunb  30492  frgrncvvdeqlem2  30502  fusgr2wsp2nb  30536  numclwlk1lem1  30571  hhcms  31406  isch3  31444  ocsh  31486  pjhtheu  31597  pjpreeq  31601  h1deoi  31752  h1dei  31753  eleigvec  32160  cvbr2  32486  cvnbtwn2  32490  cvnbtwn4  32492  mdsl2i  32525  cvmdi  32527  mdsymlem6  32611  cdj3lem3b  32643  mo5f  32688  nmo  32689  rexunirn  32691  dmrab  32696  difrab2  32697  disjunsn  32794  unipreima  32845  dfcnv2  32877  1stpreima  32909  isunit2  33420  lsmsnorb2  33578  prmidl0  33637  ssmxidl  33662  1arithufdlem4  33743  ressply1mon1p  33764  extdgfialglem1  33989  zarcls  34171  rhmpreimacnlem  34181  isrnsiga  34410  rossros  34477  omsmeas  34620  eulerpartlemr  34671  eulerpartlemgvv  34673  ballotlemodife  34795  signstfvneq0  34866  bnj251  34998  bnj252  34999  bnj257  35003  bnj290  35006  bnj1304  35114  bnj153  35175  bnj543  35188  bnj571  35201  bnj580  35208  bnj607  35211  bnj882  35221  bnj964  35238  bnj996  35251  bnj1033  35264  bnj1176  35300  bnj1186  35302  bnj1189  35304  bnj1204  35307  bnj1253  35312  bnj1452  35347  bnj1463  35350  dff15  35378  axprALT2  35405  fineqvrep  35410  fineqvac  35412  lfuhgr3  35470  cusgredgex2  35473  usgrgt2cycl  35480  2cycl2d  35489  dfacycgr1  35494  erdszelem9  35549  cvmlift2lem9  35661  cvmlift2lem13  35665  satfvsucsuc  35715  satfdm  35719  satf0  35722  fmlasucdisj  35749  satffunlem  35751  satffunlem1lem1  35752  satffunlem2lem1  35754  elmthm  35926  axinfprim  36056  axacprim  36057  xpab  36076  dfso2  36105  dford5reg  36130  dfon2lem5  36135  dfon2  36140  brtxp2  36229  brpprod3a  36234  dfom5b  36260  brcart  36280  brimg  36285  funpartlem  36292  dfrecs2  36300  cgrxfr  36405  segletr  36464  sumeq2si  36562  prodeq2si  36564  cbvprodvw2  36607  trer  36676  fneval  36712  neifg  36731  df3nandALT1  36759  andnand1  36761  nandsym1  36782  weiunlem  36823  regsfromregtco  36898  mh-infprim2bi  36907  mh-infprim3bi  36908  bj-df-sb  37122  bj-dfsbc  37124  bj-eu3f  37326  bj-csbsnlem  37388  bj-snsetex  37448  bj-elsngl  37453  bj-snglc  37454  bj-restuni  37587  bj-dfmpoa  37608  bj-imdirco  37682  mptsnunlem  37832  icorempo  37845  isbasisrelowllem2  37850  relowlpssretop  37858  rdgeqoa  37864  difunieq  37868  dffinxpf  37879  nlpineqsn  37902  curf  38097  finixpnum  38104  ptrest  38118  poimirlem1  38120  poimirlem14  38133  poimirlem16  38135  poimirlem19  38138  poimirlem25  38144  poimirlem26  38145  poimirlem27  38146  poimir  38152  cnambfre  38167  itg2addnc  38173  ftc1anc  38200  opropabco  38223  isdrngo1  38455  keridl  38531  ispridlc  38569  selconj  38599  eldmres3  38782  eldmqsres  38792  cnvepres  38803  ecinn0  38852  alrmomorn  38857  moantr  38871  dfxrn2  38884  disjressuc2  38910  inxpxrn  38917  rnxrnres  38921  coss2cnvepres  39007  refrelredund4  39218  dferALTV2  39252  dfeldisj3  39310  dfpart2  39371  dfpeters2  39473  petseq  39475  prtlem70  39481  prtlem100  39483  prtlem15  39499  islshpat  39641  lcvbr2  39646  lcvbr3  39647  lcvnbtwn2  39651  ellkr  39713  cvrval2  39898  cvrnbtwn2  39899  cvrnbtwn3  39900  cvrnbtwn4  39903  ishlat2  39977  lplnexatN  40187  islvol5  40203  dath  40360  pclfinclN  40574  lhpexle3  40636  4atex2  40701  4atex2-0bOLDN  40703  isltrn2N  40744  cdleme0nex  40914  cdleme22b  40965  cdlemg17pq  41296  cdlemg19  41308  cdlemg21  41310  cdlemg33d  41333  dibopelvalN  41767  dibopelval2  41769  dib1dim  41789  dicelval2N  41806  diclspsn  41818  lcdlss  42243  mapd1o  42272  3factsumint2  42639  3factsumint3  42640  3factsumint  42642  hashnexinj  42745  sticksstones16  42779  sticksstones21  42784  unitscyglem3  42814  supinf  42858  fimgmcyclem  43151  eu6w  43258  mzpcompact2lem  43332  fz1eqin  43350  rexrabdioph  43371  expdiophlem1  43598  dford4  43606  fnwe2lem2  43628  fgraphopab  43780  dflim6  43841  onsucf1olem  43847  onsucrn  43848  nnoeomeqom  43889  faosnf0.11b  44003  ifpidg  44067  rp-fakeinunass  44091  rp-isfinite6  44094  dfsucon  44099  elinintrab  44153  elnonrel  44161  elmapintab  44172  dfrtrcl5  44205  imaiun1  44227  coiun1  44228  rfovcnvf1od  44580  andi3or  44600  uneqsn  44601  ntrneicls00  44665  rr-groth  44875  ismnushort  44877  rr-grothshortbi  44879  2sbc5g  44992  pm14.12  44997  2sb5nd  45136  uun2221  45388  uun2221p1  45389  uun2221p2  45390  2sb5ndVD  45485  2sb5ndALT  45507  modelaxreplem3  45556  iindif2f  45738  disjinfi  45770  climuz  46318  dfxlim2  46422  cncfshift  46448  dvnmul  46517  dvnprodlem2  46521  ismbl3  46560  ismbl4  46567  stoweidlem26  46600  stoweidlem35  46609  fourierdlem54  46734  fourierdlem83  46763  fourierdlem100  46780  fourierdlem104  46784  fourierdlem109  46789  fourierdlem112  46792  smfpimcc  47382  fcoresf1ob  47667  f1cof1b  47671  f1ocof1ob  47675  2reu8i  47707  dfdfat2  47722  ffnaov  47793  an4com24  47862  4an21  47864  iccpartiltu  48028  prproropf1olem0  48108  dfgric2  48537  gpgvtxedg0  48685  gpgvtxedg1  48686  gpgprismgr4cycllem10  48726  grlimedgnedg  48753  2zrngmmgm  48874  rngcinvALTV  48898  ringcinvALTV  48932  pgrpgt2nabl  48988  islindeps  49075  lindslinindsimp1  49079  lindslinindsimp2  49085  ldepslinc  49131  blen1b  49210  coxp  49454  i0oii  49541  io1ii  49542  isthinc2  50041  isthinc3  50042  isthincd2  50058  istermc2  50096  istermc3  50097  dffun3f  50303  setrec1lem3  50310  elpglem3  50334  elpg  50335