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  2530  mo4f  2560  eu3v  2563  eu6  2567  dfeu  2588  eu2  2602  eu4  2608  2mos  2642  2mosOLD  2643  2eu4  2648  r3ex  3174  ceqsex3v  3500  ceqsex4v  3501  ceqsex8v  3503  reu2  3693  reu6  3694  reu4  3699  reu7  3700  rmo3f  3702  rmo4f  3703  2reu5lem3  3725  2reu5  3726  sbcimdv  3819  sbcg  3823  rmo3  3849  reuan  3856  dfpss2  4047  difdif  4094  raldifb  4108  inass  4187  dfss4  4228  dfin2  4230  indi  4243  indifdi  4253  undif3  4259  difin0ss  4332  inssdif0  4333  2nreu  4403  2reu4lem  4481  rexdifpr  4619  reuprg0  4662  ssdifsn  4748  ssunpr  4794  uniprg  4883  uniun  4890  uniin  4891  csbuni  4896  dfiun2g  4990  iunin2  5030  iundif2  5033  iindif2  5036  iinin2  5037  elpwpw  5061  axrep1  5230  axrep4v  5234  axrep4  5235  axrep4OLD  5236  reusv2lem4  5351  eqvinop  5442  opcom  5456  fconstmpt  5693  opeliunxp  5698  opeliun2xp  5699  xpundi  5700  elvvv  5707  opelinxp  5711  xpiindi  5789  elcnv2  5831  cnvuni  5840  dmuni  5868  brres  5946  dmres  5972  elidinxp  6004  restidsing  6013  elima3  6027  asymref  6077  imainss  6115  difxp  6125  xpdifid  6129  mptpreima  6199  coundir  6209  resco  6211  coass  6226  relrelss  6234  opreu2reurex  6255  dfpo2  6257  frpoind  6303  ordtri3or  6352  dffun2  6509  dffun2OLD  6510  dffun6  6511  dffun3  6512  dffun4  6513  dffun5  6514  dffun6f  6515  dffun7  6527  dffun8  6528  dffun9  6529  svrelfun  6572  fncnv  6573  imadif  6584  dfmpt3  6634  fcnvres  6719  fint  6721  fin  6722  dff12  6737  fores  6764  dff1o4  6790  eqfnfv3  6987  fndmin  6999  fniniseg  7014  unpreima  7017  ffnfvf  7074  fsn2  7090  tpres  7157  fconstfv  7168  dff13f  7212  dff14a  7227  dff14b  7228  isocnv2  7288  f1opr  7425  eloprabga  7478  ffnov  7495  eqfnov  7498  foov  7543  uniuni  7718  tfindsg  7817  findsg  7853  funcnvuni  7888  opabex3d  7923  opabex3rd  7924  opabex3  7925  1stconst  8056  2ndconst  8057  frxp  8082  soxp  8085  xpord3lem  8105  suppvalbr  8120  suppofssd  8159  suppcoss  8163  mpoxopovel  8176  brtpos  8191  tpostpos  8202  dfsmo2  8293  dfrecs3  8318  rdglem1  8360  tz7.49  8390  brwitnlem  8448  oeeu  8544  naddasslem2  8636  brinxper  8677  erinxp  8741  mapsncnv  8843  cbvixp  8864  cbvixpv  8865  ixpin  8873  ixpiin  8874  mptelixpg  8885  elixpsn  8887  ixpsnf1o  8888  xpassen  9012  omxpenlem  9019  sbthcl  9040  sbthfilem  9139  wemapsolem  9479  dford2  9549  inf2  9552  zfinf  9568  ttrclselem2  9655  trcl  9657  frind  9679  frr3g  9685  iscard2  9905  leweon  9940  aceq1  10046  dfac3  10050  dfac4  10051  dfac5lem2  10053  dfac5  10058  kmlem3  10082  kmlem4  10083  kmlem14  10093  kmlem15  10094  dfackm  10096  infmap2  10146  fin23lem25  10253  zorn2lem7  10431  brdom6disj  10461  zfcndrep  10543  zfcndinf  10547  fpwwe  10575  axgroth4  10761  grothprim  10763  grothtsk  10764  nqpr  10943  addsrmo  11002  mulsrmo  11003  opelreal  11059  elnnz  12515  elznn0nn  12519  peano2uz2  12598  nnwos  12850  dflt2  13084  xmullem  13200  4fvwrd4  13585  preduz  13587  elfznelfzo  13709  fzind2  13722  fsuppmapnn0fiubex  13933  hashinfxadd  14326  hashgt23el  14365  hashfun  14378  fi1uzind  14448  brfi1uzind  14449  opfi1uzind  14452  cotr2g  14918  shftdm  15013  rexfiuz  15290  cbvsum  15637  cbvsumv  15638  mertenslem2  15827  mertens  15828  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  prodmo  15878  iprodmul  15945  divalglem10  16348  ndvdssub  16355  bitsmod  16382  algcvgblem  16523  isprm2  16628  isprm4  16630  hashdvds  16721  infpn2  16860  hashbc0  16952  xpscf  17504  funcpropd  17844  isffth2  17860  eldmcoa  18007  setcinv  18032  xpccatid  18129  yonedainv  18222  ispos  18255  ispos2  18256  joinfval2  18313  meetfval2  18327  istsr2  18525  isnsg2  19070  isnsg4  19081  isgim  19176  oppgid  19270  oppgcntz  19278  symgfix2  19330  efgval2  19638  iscyg2  19796  dmdprdd  19915  subgdmdprd  19950  issrg  20108  oppr1  20270  opprunit  20297  opprirred  20342  isrnghm  20361  isrhm  20398  issubrng  20467  subsubrng2  20484  subsubrg2  20519  rngcinv  20557  ringcinv  20591  isdomn2  20631  isdomn2OLD  20632  islmim  21001  lbsextg  21104  lidlnz  21184  resubdrg  21550  unocv  21622  pjfval2  21651  islinds2  21755  opsrtoslem1  21995  mdetunilem8  22539  istop2g  22816  isbasis2g  22868  tgval2  22876  isclo2  23008  isnrm2  23278  is1stc2  23362  llyi  23394  isfbas2  23755  elfg  23791  ufinffr  23849  isfcls  23929  alexsubALTlem2  23968  alexsubALTlem3  23969  cnextcn  23987  ustfilxp  24133  iscusp2  24222  metustid  24475  isclmp  25030  iscvsp  25061  tcphcph  25170  iscau3  25211  caucfil  25216  mdegleb  26002  ellogdm  26581  dvdsflsumcom  27131  logfac2  27161  dchrelbas3  27182  dchrvmasumlema  27444  nosupno  27648  noinfno  27663  noinfbnd1lem1  27668  dmscut  27757  made0  27822  mulsproplem5  28063  norecdiv  28133  elnnzs  28329  uzsind  28333  zsoring  28336  legtrid  28571  outpasch  28735  axcontlem5  28948  axcontlem6  28949  axcontlem7  28950  nb3grpr2  29363  iscplgr  29395  dfpth2  29709  pthdlem1  29746  wwlksnextinj  29879  usgr2wspthon  29945  rusgrnumwwlkl1  29948  isclwwlk  29963  clwwlkccatlem  29968  clwwlknon2x  30082  iseupthf1o  30181  frcond3  30248  frgr3v  30254  4cycl2vnunb  30269  frgrncvvdeqlem2  30279  fusgr2wsp2nb  30313  numclwlk1lem1  30348  hhcms  31182  isch3  31220  ocsh  31262  pjhtheu  31373  pjpreeq  31377  h1deoi  31528  h1dei  31529  eleigvec  31936  cvbr2  32262  cvnbtwn2  32266  cvnbtwn4  32268  mdsl2i  32301  cvmdi  32303  mdsymlem6  32387  cdj3lem3b  32419  mo5f  32468  nmo  32469  rexunirn  32471  dmrab  32476  difrab2  32477  disjunsn  32573  unipreima  32617  dfcnv2  32650  1stpreima  32680  isunit2  33207  lsmsnorb2  33356  prmidl0  33414  ssmxidl  33438  1arithufdlem4  33511  ressply1mon1p  33530  zarcls  33857  rhmpreimacnlem  33867  isrnsiga  34096  rossros  34163  omsmeas  34307  eulerpartlemr  34358  eulerpartlemgvv  34360  ballotlemodife  34482  plymulx  34532  signstfvneq0  34556  bnj251  34685  bnj252  34686  bnj257  34690  bnj290  34693  bnj1304  34802  bnj153  34863  bnj543  34876  bnj571  34889  bnj580  34896  bnj607  34899  bnj882  34909  bnj964  34926  bnj996  34939  bnj1033  34952  bnj1176  34988  bnj1186  34990  bnj1189  34992  bnj1204  34995  bnj1253  35000  bnj1452  35035  bnj1463  35038  dff15  35067  fineqvrep  35078  fineqvac  35080  lfuhgr3  35100  cusgredgex2  35103  usgrgt2cycl  35110  2cycl2d  35119  dfacycgr1  35124  erdszelem9  35179  cvmlift2lem9  35291  cvmlift2lem13  35295  satfvsucsuc  35345  satfdm  35349  satf0  35352  fmlasucdisj  35379  satffunlem  35381  satffunlem1lem1  35382  satffunlem2lem1  35384  elmthm  35556  axinfprim  35686  axacprim  35687  xpab  35706  dfso2  35735  dford5reg  35763  dfon2lem5  35768  dfon2  35773  brtxp2  35862  brpprod3a  35867  dfom5b  35893  brcart  35913  brimg  35918  funpartlem  35923  dfrecs2  35931  cgrxfr  36036  segletr  36095  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36228  trer  36297  fneval  36333  neifg  36352  df3nandALT1  36380  andnand1  36382  nandsym1  36403  weiunlem2  36444  bj-eu3f  36822  bj-csbsnlem  36884  bj-snsetex  36944  bj-elsngl  36949  bj-snglc  36950  bj-restuni  37078  bj-dfmpoa  37099  bj-imdirco  37171  mptsnunlem  37319  icorempo  37332  isbasisrelowllem2  37337  relowlpssretop  37345  rdgeqoa  37351  difunieq  37355  dffinxpf  37366  nlpineqsn  37389  curf  37585  finixpnum  37592  ptrest  37606  poimirlem1  37608  poimirlem14  37621  poimirlem16  37623  poimirlem19  37626  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimir  37640  cnambfre  37655  itg2addnc  37661  ftc1anc  37688  opropabco  37711  isdrngo1  37943  keridl  38019  ispridlc  38057  selconj  38087  eldmres3  38258  eldmqsres  38268  cnvepres  38279  ecinn0  38328  alrmomorn  38333  moantr  38339  dfxrn2  38351  disjressuc2  38367  inxpxrn  38374  rnxrnres  38378  coss2cnvepres  38402  refrelredund4  38619  dferALTV2  38653  dfeldisj3  38704  dfpart2  38754  prtlem70  38843  prtlem100  38845  prtlem15  38861  islshpat  39003  lcvbr2  39008  lcvbr3  39009  lcvnbtwn2  39013  ellkr  39075  cvrval2  39260  cvrnbtwn2  39261  cvrnbtwn3  39262  cvrnbtwn4  39265  ishlat2  39339  lplnexatN  39550  islvol5  39566  dath  39723  pclfinclN  39937  lhpexle3  39999  4atex2  40064  4atex2-0bOLDN  40066  isltrn2N  40107  cdleme0nex  40277  cdleme22b  40328  cdlemg17pq  40659  cdlemg19  40671  cdlemg21  40673  cdlemg33d  40696  dibopelvalN  41130  dibopelval2  41132  dib1dim  41152  dicelval2N  41169  diclspsn  41181  lcdlss  41606  mapd1o  41635  3factsumint2  42003  3factsumint3  42004  3factsumint  42006  hashnexinj  42109  sticksstones16  42143  sticksstones21  42148  unitscyglem3  42178  supinf  42223  fimgmcyclem  42514  eu6w  42657  mzpcompact2lem  42732  fz1eqin  42750  rexrabdioph  42775  expdiophlem1  43003  dford4  43011  fnwe2lem2  43033  fgraphopab  43185  dflim6  43246  onsucf1olem  43252  onsucrn  43253  nnoeomeqom  43294  faosnf0.11b  43409  ifpidg  43473  rp-fakeinunass  43497  rp-isfinite6  43500  dfsucon  43505  elinintrab  43559  elnonrel  43567  elmapintab  43578  dfrtrcl5  43611  imaiun1  43633  coiun1  43634  rfovcnvf1od  43986  andi3or  44006  uneqsn  44007  ntrneicls00  44071  rr-groth  44281  ismnushort  44283  rr-grothshortbi  44285  2sbc5g  44398  pm14.12  44403  2sb5nd  44543  uun2221  44795  uun2221p1  44796  uun2221p2  44797  2sb5ndVD  44892  2sb5ndALT  44914  modelaxreplem3  44963  iindif2f  45147  disjinfi  45179  climuz  45735  dfxlim2  45839  cncfshift  45865  dvnmul  45934  dvnprodlem2  45938  ismbl3  45977  ismbl4  45984  stoweidlem26  46017  stoweidlem35  46026  fourierdlem54  46151  fourierdlem83  46180  fourierdlem100  46197  fourierdlem104  46201  fourierdlem109  46206  fourierdlem112  46209  smfpimcc  46799  fcoresf1ob  47067  f1cof1b  47071  f1ocof1ob  47075  2reu8i  47107  dfdfat2  47122  ffnaov  47193  an4com24  47262  4an21  47264  iccpartiltu  47416  prproropf1olem0  47496  dfgric2  47908  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem10  48087  2zrngmmgm  48233  rngcinvALTV  48257  ringcinvALTV  48291  pgrpgt2nabl  48347  islindeps  48435  lindslinindsimp1  48439  lindslinindsimp2  48445  ldepslinc  48491  blen1b  48570  coxp  48814  i0oii  48901  io1ii  48902  isthinc2  49402  isthinc3  49403  isthincd2  49419  istermc2  49457  istermc3  49458  dffun3f  49664  setrec1lem3  49671  elpglem3  49695  elpg  49696