Theorem anbi2i 634

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi1ci  637  anbi12i  639  bianass  654  an42  669  anandir  689  dfbi3  1065  dn1  1073  dfifp3  1081  ifpdfbiOLD  1087  4anpull2OLD  1383  an3andi  1513  an33rean  1514  anxordi  1556  cadcoma  1642  nic-mpALT  1702  nic-axALT  1704  3exdistr  1990  4exdistr  1991  19.27v  2025  19.27  2263  19.41  2271  2sb5  2313  dfsb7  2314  dfeumo  2564  mo4f  2595  eu3v  2598  eu6  2602  dfeu  2623  eu2  2637  eu4  2643  2mos  2677  2eu4  2682  r3ex  3204  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  reu2  3688  reu6  3689  reu4  3694  reu7  3695  rmo3f  3697  rmo4f  3698  2reu5lem3  3720  2reu5  3721  sbcimdv  3812  sbcg  3816  rmo3  3842  reuan  3850  dfpss2  4042  difdif  4089  raldifb  4103  inass  4180  dfss4  4222  dfin2  4224  indi  4237  indifdi  4247  undif3  4253  difin0ss  4328  inssdif0OLD  4330  2nreu  4409  2reu4lem  4484  rexdifpr  4625  reuprg0  4668  ssdifsn  4756  ssunpr  4799  uniprg  4888  uniun  4895  uniinOLD  4897  csbuni  4903  dfiun2g  4994  iunin2  5035  iundif2  5038  iindif2  5043  iinin2  5044  elpwpw  5068  axrep1  5239  axrep4v  5243  axrep4  5244  axrep4OLD  5245  reusv2lem4  5372  eqvinop  5469  opcom  5484  fconstmpt  5723  opeliunxp  5728  opeliun2xp  5729  xpundi  5730  elvvv  5737  opelinxp  5741  xpiindi  5821  elcnv2  5863  cnvuni  5876  dmuni  5904  brres  5985  dmres  6011  elidinxp  6046  restidsing  6055  elima3  6069  asymref  6116  imainss  6151  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  mptpreima  6239  coundir  6249  resco  6251  coass  6267  relrelss  6274  opreu2reurex  6295  dfpo2  6297  frpoind  6343  ordtri3or  6393  dffun2  6546  dffun6  6547  dffun3  6548  dffun4  6549  dffun5  6550  dffun6f  6551  dffun7  6563  dffun8  6564  dffun9  6565  svrelfun  6608  fncnv  6609  imadif  6620  dfmpt3  6669  fcnvres  6755  fint  6757  fin  6758  dff12  6773  fores  6802  dff1o4  6829  eqfnfv3  7027  fndmin  7040  fniniseg  7055  unpreima  7058  ffnfvf  7115  fsn2  7132  tpres  7199  fconstfv  7210  dff13f  7253  dff14a  7268  dff14b  7269  isocnv2  7329  f1opr  7466  eloprabga  7519  ffnov  7536  eqfnov  7539  foov  7584  uniuni  7757  tfindsg  7853  findsg  7890  funcnvuni  7925  opabex3d  7958  opabex3rd  7959  opabex3  7960  1stconst  8091  2ndconst  8092  frxp  8118  soxp  8121  xpord3lem  8141  suppvalbr  8156  suppofssd  8195  suppcoss  8199  mpoxopovel  8212  brtpos  8227  tpostpos  8238  dfsmo2  8330  dfrecs3  8355  rdglem1  8398  tz7.49  8428  brwitnlem  8488  oeeu  8585  naddasslem2  8678  brinxper  8720  erinxp  8785  mapsncnv  8887  cbvixp  8908  cbvixpv  8909  ixpin  8917  ixpiin  8918  mptelixpg  8929  elixpsn  8931  ixpsnf1o  8932  xpassen  9055  omxpenlem  9062  sbthcl  9083  sbthfilem  9178  wemapsolem  9508  dford2  9585  inf2  9588  zfinf  9604  ttrclselem2  9691  trcl  9693  frind  9718  frr3g  9724  iscard2  9958  leweon  9991  aceq1  10097  dfac3  10101  dfac4  10102  dfac5lem2  10104  dfac5  10108  kmlem3  10132  kmlem4  10133  kmlem14  10143  kmlem15  10144  dfackm  10146  infmap2  10196  fin23lem25  10303  zorn2lem7  10481  brdom6disj  10511  zfcndrep  10594  zfcndinf  10598  fpwwe  10626  axgroth4  10812  grothprim  10814  grothtsk  10815  nqpr  10994  addsrmo  11053  mulsrmo  11054  opelreal  11110  elnnz  12596  elznn0nn  12600  peano2uz2  12679  nnwos  12934  dflt2  13168  xmullem  13285  4fvwrd4  13672  preduz  13674  elfznelfzo  13798  fzind2  13813  fsuppmapnn0fiubex  14024  hashinfxadd  14417  hashgt23el  14457  hashfun  14470  fi1uzind  14540  brfi1uzind  14541  opfi1uzind  14544  cotr2g  15009  shftdm  15104  rexfiuz  15395  cbvsum  15742  cbvsumv  15743  mertenslem2  15935  mertens  15936  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  prodmo  15986  iprodmul  16053  divalglem10  16455  ndvdssub  16462  bitsmod  16489  algcvgblem  16630  isprm2  16735  isprm4  16737  hashdvds  16829  infpn2  16968  hashbc0  17060  xpscf  17614  funcpropd  17954  isffth2  17970  eldmcoa  18117  setcinv  18142  xpccatid  18239  yonedainv  18332  ispos  18365  ispos2  18366  joinfval2  18423  meetfval2  18437  istsr2  18635  isnsg2  19217  isnsg4  19228  isgim  19327  oppgid  19421  oppgcntz  19429  symgfix2  19481  efgval2  19789  iscyg2  19947  dmdprdd  20066  subgdmdprd  20101  issrg  20265  oppr1  20428  opprunit  20455  opprirred  20500  isrnghm  20519  isrhm  20557  issubrng  20646  subsubrng2  20663  subsubrg2  20698  rngcinv  20736  ringcinv  20770  isdomn2  20810  islmim  21183  lbsextg  21286  lidlnz  21376  prmidl0  21478  resubdrg  21758  unocv  21830  pjfval2  21859  islinds2  21963  opsrtoslem1  22206  mdetunilem8  22776  istop2g  23053  isbasis2g  23105  tgval2  23113  isclo2  23245  isnrm2  23515  is1stc2  23599  llyi  23631  isfbas2  23992  elfg  24028  ufinffr  24086  isfcls  24166  alexsubALTlem2  24205  alexsubALTlem3  24206  cnextcn  24224  ustfilxp  24370  iscusp2  24458  metustid  24711  isclmp  25256  iscvsp  25287  tcphcph  25396  iscau3  25437  caucfil  25442  mdegleb  26221  plymulidp  26443  ellogdm  26804  dvdsflsumcom  27352  logfac2  27381  dchrelbas3  27402  dchrvmasumlema  27664  nosupno  27867  noinfno  27882  noinfbnd1lem1  27887  dmcuts  27984  made0  28056  mulsproplem5  28313  norecdiv  28383  elnnzs  28594  uzsind  28598  zsoring  28602  legtrid  28860  outpasch  29037  tgaltai  29217  axcontlem5  29318  axcontlem6  29319  axcontlem7  29320  nb3grpr2  29733  iscplgr  29765  dfpth2  30078  pthdlem1  30115  wwlksnextinj  30248  usgr2wspthon  30317  rusgrnumwwlkl1  30320  isclwwlk  30335  clwwlkccatlem  30340  clwwlknon2x  30454  iseupthf1o  30553  frcond3  30620  frgr3v  30626  4cycl2vnunb  30641  frgrncvvdeqlem2  30651  fusgr2wsp2nb  30685  numclwlk1lem1  30720  hhcms  31555  isch3  31593  ocsh  31635  pjhtheu  31746  pjpreeq  31750  h1deoi  31901  h1dei  31902  eleigvec  32309  cvbr2  32635  cvnbtwn2  32639  cvnbtwn4  32641  mdsl2i  32674  cvmdi  32676  mdsymlem6  32760  cdj3lem3b  32792  mo5f  32835  nmo  32836  rexunirn  32838  dmrab  32843  difrab2  32844  disjunsn  32939  unipreima  32988  dfcnv2  33020  1stpreima  33052  isunit2  33559  lsmsnorb2  33705  ssmxidl  33757  1arithufdlem4  33837  ressply1mon1p  33858  extdgfialglem1  34082  zarcls  34264  rhmpreimacnlem  34274  isrnsiga  34503  rossros  34570  omsmeas  34713  eulerpartlemr  34764  eulerpartlemgvv  34766  ballotlemodife  34888  signstfvneq0  34959  bnj251  35091  bnj252  35092  bnj257  35096  bnj290  35099  bnj1304  35207  bnj153  35268  bnj543  35281  bnj571  35294  bnj580  35301  bnj607  35304  bnj882  35314  bnj964  35331  bnj996  35344  bnj1033  35357  bnj1176  35393  bnj1186  35395  bnj1189  35397  bnj1204  35400  bnj1253  35405  bnj1452  35440  bnj1463  35443  dff15  35472  axprALT2  35503  fineqvrep  35527  fineqvac  35529  kardexen  35576  lfuhgr3  35612  cusgredgex2  35615  usgrgt2cycl  35622  2cycl2d  35631  dfacycgr1  35636  erdszelem9  35691  cvmlift2lem9  35803  cvmlift2lem13  35807  satfvsucsuc  35857  satfdm  35861  satf0  35864  fmlasucdisj  35891  satffunlem  35893  satffunlem1lem1  35894  satffunlem2lem1  35896  elmthm  36068  axinfprim  36198  axacprim  36199  xpab  36218  dfso2  36247  dford5reg  36272  dfon2lem5  36277  dfon2  36282  brtxp2  36371  brpprod3a  36376  dfom5b  36402  brcart  36422  brimg  36427  funpartlem  36434  dfrecs2  36442  cgrxfr  36547  segletr  36606  sumeq2si  36734  prodeq2si  36736  cbvprodvw2  36779  trer  36847  fneval  36883  neifg  36902  df3nandALT1  36930  andnand1  36932  nandsym1  36953  weiunlem  36994  regsfromregtco  37069  mh-infprim2bi  37078  mh-infprim3bi  37079  bj-df-sb  37292  bj-dfsbc  37294  bj-eu3f  37496  bj-csbsnlem  37558  bj-snsetex  37619  bj-elsngl  37624  bj-snglc  37625  bj-restuni  37759  bj-dfmpoa  37780  bj-imdirco  37854  mptsnunlem  38004  icorempo  38017  isbasisrelowllem2  38022  relowlpssretop  38030  rdgeqoa  38036  difunieq  38040  dffinxpf  38051  nlpineqsn  38074  curf  38269  finixpnum  38276  ptrest  38290  poimirlem1  38292  poimirlem14  38305  poimirlem16  38307  poimirlem19  38310  poimirlem25  38316  poimirlem26  38317  poimirlem27  38318  poimir  38324  cnambfre  38339  itg2addnc  38345  ftc1anc  38372  opropabco  38395  isdrngo1  38627  keridl  38703  ispridlc  38741  selconj  38769  eldmres3  38952  eldmqsres  38962  cnvepres  38973  ecinn0  39022  alrmomorn  39027  moantr  39041  dfxrn2  39054  disjressuc2  39080  inxpxrn  39087  rnxrnres  39091  coss2cnvepres  39177  refrelredund4  39388  dferALTV2  39422  dfeldisj3  39480  dfpart2  39541  dfpeters2  39643  petseq  39645  prtlem70  39651  prtlem100  39653  prtlem15  39669  islshpat  39811  lcvbr2  39816  lcvbr3  39817  lcvnbtwn2  39821  ellkr  39883  cvrval2  40068  cvrnbtwn2  40069  cvrnbtwn3  40070  cvrnbtwn4  40073  ishlat2  40147  lplnexatN  40357  islvol5  40373  dath  40530  pclfinclN  40744  lhpexle3  40806  4atex2  40871  4atex2-0bOLDN  40873  isltrn2N  40914  cdleme0nex  41084  cdleme22b  41135  cdlemg17pq  41466  cdlemg19  41478  cdlemg21  41480  cdlemg33d  41503  dibopelvalN  41937  dibopelval2  41939  dib1dim  41959  dicelval2N  41976  diclspsn  41988  lcdlss  42413  mapd1o  42442  3factsumint2  42809  3factsumint3  42810  3factsumint  42812  hashnexinj  42915  sticksstones16  42949  sticksstones21  42954  unitscyglem3  42984  supinf  43030  fimgmcyclem  43321  eu6w  43428  mzpcompact2lem  43502  fz1eqin  43520  rexrabdioph  43541  expdiophlem1  43768  dford4  43776  fnwe2lem2  43798  fgraphopab  43950  dflim6  44011  onsucf1olem  44017  onsucrn  44018  nnoeomeqom  44059  faosnf0.11b  44173  ifpidg  44237  rp-fakeinunass  44261  rp-isfinite6  44264  dfsucon  44269  elinintrab  44323  elnonrel  44331  elmapintab  44342  dfrtrcl5  44375  imaiun1  44397  coiun1  44398  rfovcnvf1od  44750  andi3or  44770  uneqsn  44771  ntrneicls00  44835  rr-groth  45029  ismnushort  45031  rr-grothshortbi  45033  2sbc5g  45146  pm14.12  45151  2sb5nd  45289  uun2221  45541  uun2221p1  45542  uun2221p2  45543  2sb5ndVD  45638  2sb5ndALT  45660  modelaxreplem3  45709  iindif2f  45898  disjinfi  45930  climuz  46478  dfxlim2  46582  cncfshift  46608  dvnmul  46677  dvnprodlem2  46681  ismbl3  46720  ismbl4  46727  stoweidlem26  46760  stoweidlem35  46769  fourierdlem54  46894  fourierdlem83  46923  fourierdlem100  46940  fourierdlem104  46944  fourierdlem109  46949  fourierdlem112  46952  smfpimcc  47542  fcoresf1ob  47830  f1cof1b  47834  f1ocof1ob  47838  2reu8i  47870  dfdfat2  47885  ffnaov  47956  an4com24  48025  4an21  48027  iccpartiltu  48191  prproropf1olem0  48271  dfgric2  48700  gpgvtxedg0  48848  gpgvtxedg1  48849  gpgprismgr4cycllem10  48889  grlimedgnedg  48916  2zrngmmgm  49037  rngcinvALTV  49061  ringcinvALTV  49095  isprmrng  49121  pgrpgt2nabl  49166  islindeps  49253  lindslinindsimp1  49257  lindslinindsimp2  49263  ldepslinc  49309  blen1b  49388  coxp  49631  i0oii  49718  io1ii  49719  isthinc2  50218  isthinc3  50219  isthincd2  50235  istermc2  50273  istermc3  50274  dffun3f  50480  setrec1lem3  50487  elpglem3  50511  elpg  50512  alsanmo  50608  ralsanmo  50609  2alsraln0  50615  2alsraln0id  50616