Theorem anbi2i 623

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  626  anbi12i  628  bianass  642  an42  657  anandir  677  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1526  cadcoma  1612  nic-mpALT  1672  nic-axALT  1674  3exdistr  1960  4exdistr  1961  19.27v  1995  19.27  2228  19.41  2236  2sb5  2278  dfsb7  2279  dfeumo  2531  mo4f  2561  eu3v  2564  eu6  2568  dfeu  2589  eu2  2603  eu4  2609  2mos  2643  2mosOLD  2644  2eu4  2649  r3ex  3177  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  reu2  3699  reu6  3700  reu4  3705  reu7  3706  rmo3f  3708  rmo4f  3709  2reu5lem3  3731  2reu5  3732  sbcimdv  3825  sbcg  3829  rmo3  3855  reuan  3862  dfpss2  4054  difdif  4101  raldifb  4115  inass  4194  dfss4  4235  dfin2  4237  indi  4250  indifdi  4260  undif3  4266  difin0ss  4339  inssdif0  4340  2nreu  4410  2reu4lem  4488  rexdifpr  4626  reuprg0  4669  ssdifsn  4755  ssunpr  4801  uniprg  4890  uniun  4897  uniin  4898  csbuni  4903  dfiun2g  4997  iunin2  5038  iundif2  5041  iindif2  5044  iinin2  5045  elpwpw  5069  axrep1  5238  axrep4v  5242  axrep4  5243  axrep4OLD  5244  reusv2lem4  5359  eqvinop  5450  opcom  5464  fconstmpt  5703  opeliunxp  5708  opeliun2xp  5709  xpundi  5710  elvvv  5717  opelinxp  5721  xpiindi  5802  elcnv2  5844  cnvuni  5853  dmuni  5881  brres  5960  dmres  5986  elidinxp  6018  restidsing  6027  elima3  6041  asymref  6092  imainss  6130  difxp  6140  xpdifid  6144  mptpreima  6214  coundir  6224  resco  6226  coass  6241  relrelss  6249  opreu2reurex  6270  dfpo2  6272  frpoind  6318  ordtri3or  6367  dffun2  6524  dffun2OLD  6525  dffun2OLDOLD  6526  dffun6  6527  dffun3  6528  dffun3OLD  6529  dffun4  6530  dffun5  6531  dffun6f  6532  dffun7  6546  dffun8  6547  dffun9  6548  svrelfun  6591  fncnv  6592  imadif  6603  dfmpt3  6655  fcnvres  6740  fint  6742  fin  6743  dff12  6758  fores  6785  dff1o4  6811  eqfnfv3  7008  fndmin  7020  fniniseg  7035  unpreima  7038  ffnfvf  7095  fsn2  7111  tpres  7178  fconstfv  7189  dff13f  7233  dff14a  7248  dff14b  7249  isocnv2  7309  f1opr  7448  eloprabga  7501  ffnov  7518  eqfnov  7521  foov  7566  uniuni  7741  tfindsg  7840  findsg  7876  funcnvuni  7911  opabex3d  7947  opabex3rd  7948  opabex3  7949  1stconst  8082  2ndconst  8083  frxp  8108  soxp  8111  xpord3lem  8131  suppvalbr  8146  suppofssd  8185  suppcoss  8189  mpoxopovel  8202  brtpos  8217  tpostpos  8228  dfsmo2  8319  dfrecs3  8344  rdglem1  8386  tz7.49  8416  brwitnlem  8474  oeeu  8570  naddasslem2  8662  brinxper  8703  erinxp  8767  mapsncnv  8869  cbvixp  8890  cbvixpv  8891  ixpin  8899  ixpiin  8900  mptelixpg  8911  elixpsn  8913  ixpsnf1o  8914  xpassen  9040  omxpenlem  9047  sbthcl  9069  sbthfilem  9168  wemapsolem  9510  dford2  9580  inf2  9583  zfinf  9599  ttrclselem2  9686  trcl  9688  frind  9710  frr3g  9716  iscard2  9936  leweon  9971  aceq1  10077  dfac3  10081  dfac4  10082  dfac5lem2  10084  dfac5  10089  kmlem3  10113  kmlem4  10114  kmlem14  10124  kmlem15  10125  dfackm  10127  infmap2  10177  fin23lem25  10284  zorn2lem7  10462  brdom6disj  10492  zfcndrep  10574  zfcndinf  10578  fpwwe  10606  axgroth4  10792  grothprim  10794  grothtsk  10795  nqpr  10974  addsrmo  11033  mulsrmo  11034  opelreal  11090  elnnz  12546  elznn0nn  12550  peano2uz2  12629  nnwos  12881  dflt2  13115  xmullem  13231  4fvwrd4  13616  preduz  13618  elfznelfzo  13740  fzind2  13753  fsuppmapnn0fiubex  13964  hashinfxadd  14357  hashgt23el  14396  hashfun  14409  fi1uzind  14479  brfi1uzind  14480  opfi1uzind  14483  cotr2g  14949  shftdm  15044  rexfiuz  15321  cbvsum  15668  cbvsumv  15669  mertenslem2  15858  mertens  15859  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  prodmo  15909  iprodmul  15976  divalglem10  16379  ndvdssub  16386  bitsmod  16413  algcvgblem  16554  isprm2  16659  isprm4  16661  hashdvds  16752  infpn2  16891  hashbc0  16983  xpscf  17535  funcpropd  17871  isffth2  17887  eldmcoa  18034  setcinv  18059  xpccatid  18156  yonedainv  18249  ispos  18282  ispos2  18283  joinfval2  18340  meetfval2  18354  istsr2  18550  isnsg2  19095  isnsg4  19106  isgim  19201  oppgid  19295  oppgcntz  19303  symgfix2  19353  efgval2  19661  iscyg2  19819  dmdprdd  19938  subgdmdprd  19973  issrg  20104  oppr1  20266  opprunit  20293  opprirred  20338  isrnghm  20357  isrhm  20394  issubrng  20463  subsubrng2  20480  subsubrg2  20515  rngcinv  20553  ringcinv  20587  isdomn2  20627  isdomn2OLD  20628  islmim  20976  lbsextg  21079  lidlnz  21159  resubdrg  21524  unocv  21596  pjfval2  21625  islinds2  21729  opsrtoslem1  21969  mdetunilem8  22513  istop2g  22790  isbasis2g  22842  tgval2  22850  isclo2  22982  isnrm2  23252  is1stc2  23336  llyi  23368  isfbas2  23729  elfg  23765  ufinffr  23823  isfcls  23903  alexsubALTlem2  23942  alexsubALTlem3  23943  cnextcn  23961  ustfilxp  24107  iscusp2  24196  metustid  24449  isclmp  25004  iscvsp  25035  tcphcph  25144  iscau3  25185  caucfil  25190  mdegleb  25976  ellogdm  26555  dvdsflsumcom  27105  logfac2  27135  dchrelbas3  27156  dchrvmasumlema  27418  nosupno  27622  noinfno  27637  noinfbnd1lem1  27642  dmscut  27730  made0  27792  mulsproplem5  28030  norecdiv  28100  elnnzs  28296  uzsind  28300  legtrid  28525  outpasch  28689  axcontlem5  28902  axcontlem6  28903  axcontlem7  28904  nb3grpr2  29317  iscplgr  29349  dfpth2  29666  pthdlem1  29703  wwlksnextinj  29836  usgr2wspthon  29902  rusgrnumwwlkl1  29905  isclwwlk  29920  clwwlkccatlem  29925  clwwlknon2x  30039  iseupthf1o  30138  frcond3  30205  frgr3v  30211  4cycl2vnunb  30226  frgrncvvdeqlem2  30236  fusgr2wsp2nb  30270  numclwlk1lem1  30305  hhcms  31139  isch3  31177  ocsh  31219  pjhtheu  31330  pjpreeq  31334  h1deoi  31485  h1dei  31486  eleigvec  31893  cvbr2  32219  cvnbtwn2  32223  cvnbtwn4  32225  mdsl2i  32258  cvmdi  32260  mdsymlem6  32344  cdj3lem3b  32376  mo5f  32425  nmo  32426  rexunirn  32428  dmrab  32433  difrab2  32434  disjunsn  32530  unipreima  32574  dfcnv2  32607  1stpreima  32637  isunit2  33198  lsmsnorb2  33370  prmidl0  33428  ssmxidl  33452  1arithufdlem4  33525  ressply1mon1p  33544  zarcls  33871  rhmpreimacnlem  33881  isrnsiga  34110  rossros  34177  omsmeas  34321  eulerpartlemr  34372  eulerpartlemgvv  34374  ballotlemodife  34496  plymulx  34546  signstfvneq0  34570  bnj251  34699  bnj252  34700  bnj257  34704  bnj290  34707  bnj1304  34816  bnj153  34877  bnj543  34890  bnj571  34903  bnj580  34910  bnj607  34913  bnj882  34923  bnj964  34940  bnj996  34953  bnj1033  34966  bnj1176  35002  bnj1186  35004  bnj1189  35006  bnj1204  35009  bnj1253  35014  bnj1452  35049  bnj1463  35052  dff15  35081  fineqvrep  35092  fineqvac  35094  lfuhgr3  35114  cusgredgex2  35117  usgrgt2cycl  35124  2cycl2d  35133  dfacycgr1  35138  erdszelem9  35193  cvmlift2lem9  35305  cvmlift2lem13  35309  satfvsucsuc  35359  satfdm  35363  satf0  35366  fmlasucdisj  35393  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  elmthm  35570  axinfprim  35700  axacprim  35701  xpab  35720  dfso2  35749  dford5reg  35777  dfon2lem5  35782  dfon2  35787  brtxp2  35876  brpprod3a  35881  dfom5b  35907  brcart  35927  brimg  35932  funpartlem  35937  dfrecs2  35945  cgrxfr  36050  segletr  36109  sumeq2si  36197  prodeq2si  36199  cbvprodvw2  36242  trer  36311  fneval  36347  neifg  36366  df3nandALT1  36394  andnand1  36396  nandsym1  36417  weiunlem2  36458  bj-eu3f  36836  bj-csbsnlem  36898  bj-snsetex  36958  bj-elsngl  36963  bj-snglc  36964  bj-restuni  37092  bj-dfmpoa  37113  bj-imdirco  37185  mptsnunlem  37333  icorempo  37346  isbasisrelowllem2  37351  relowlpssretop  37359  rdgeqoa  37365  difunieq  37369  dffinxpf  37380  nlpineqsn  37403  curf  37599  finixpnum  37606  ptrest  37620  poimirlem1  37622  poimirlem14  37635  poimirlem16  37637  poimirlem19  37640  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimir  37654  cnambfre  37669  itg2addnc  37675  ftc1anc  37702  opropabco  37725  isdrngo1  37957  keridl  38033  ispridlc  38071  selconj  38101  eldmres3  38272  eldmqsres  38282  cnvepres  38293  ecinn0  38342  alrmomorn  38347  moantr  38353  dfxrn2  38365  disjressuc2  38381  inxpxrn  38388  rnxrnres  38392  coss2cnvepres  38416  refrelredund4  38633  dferALTV2  38667  dfeldisj3  38718  dfpart2  38768  prtlem70  38857  prtlem100  38859  prtlem15  38875  islshpat  39017  lcvbr2  39022  lcvbr3  39023  lcvnbtwn2  39027  ellkr  39089  cvrval2  39274  cvrnbtwn2  39275  cvrnbtwn3  39276  cvrnbtwn4  39279  ishlat2  39353  lplnexatN  39564  islvol5  39580  dath  39737  pclfinclN  39951  lhpexle3  40013  4atex2  40078  4atex2-0bOLDN  40080  isltrn2N  40121  cdleme0nex  40291  cdleme22b  40342  cdlemg17pq  40673  cdlemg19  40685  cdlemg21  40687  cdlemg33d  40710  dibopelvalN  41144  dibopelval2  41146  dib1dim  41166  dicelval2N  41183  diclspsn  41195  lcdlss  41620  mapd1o  41649  3factsumint2  42017  3factsumint3  42018  3factsumint  42020  hashnexinj  42123  sticksstones16  42157  sticksstones21  42162  unitscyglem3  42192  supinf  42237  fimgmcyclem  42528  eu6w  42671  mzpcompact2lem  42746  fz1eqin  42764  rexrabdioph  42789  expdiophlem1  43017  dford4  43025  fnwe2lem2  43047  fgraphopab  43199  dflim6  43260  onsucf1olem  43266  onsucrn  43267  nnoeomeqom  43308  faosnf0.11b  43423  ifpidg  43487  rp-fakeinunass  43511  rp-isfinite6  43514  dfsucon  43519  elinintrab  43573  elnonrel  43581  elmapintab  43592  dfrtrcl5  43625  imaiun1  43647  coiun1  43648  rfovcnvf1od  44000  andi3or  44020  uneqsn  44021  ntrneicls00  44085  rr-groth  44295  ismnushort  44297  rr-grothshortbi  44299  2sbc5g  44412  pm14.12  44417  2sb5nd  44557  uun2221  44809  uun2221p1  44810  uun2221p2  44811  2sb5ndVD  44906  2sb5ndALT  44928  modelaxreplem3  44977  iindif2f  45161  disjinfi  45193  climuz  45749  dfxlim2  45853  cncfshift  45879  dvnmul  45948  dvnprodlem2  45952  ismbl3  45991  ismbl4  45998  stoweidlem26  46031  stoweidlem35  46040  fourierdlem54  46165  fourierdlem83  46194  fourierdlem100  46211  fourierdlem104  46215  fourierdlem109  46220  fourierdlem112  46223  smfpimcc  46813  fcoresf1ob  47078  f1cof1b  47082  f1ocof1ob  47086  2reu8i  47118  dfdfat2  47133  ffnaov  47204  an4com24  47273  4an21  47275  iccpartiltu  47427  prproropf1olem0  47507  dfgric2  47919  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgprismgr4cycllem10  48098  2zrngmmgm  48244  rngcinvALTV  48268  ringcinvALTV  48302  pgrpgt2nabl  48358  islindeps  48446  lindslinindsimp1  48450  lindslinindsimp2  48456  ldepslinc  48502  blen1b  48581  coxp  48825  i0oii  48912  io1ii  48913  isthinc2  49413  isthinc3  49414  isthincd2  49430  istermc2  49468  istermc3  49469  dffun3f  49675  setrec1lem3  49682  elpglem3  49706  elpg  49707