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  17840  isffth2  17856  eldmcoa  18003  setcinv  18028  xpccatid  18125  yonedainv  18218  ispos  18251  ispos2  18252  joinfval2  18309  meetfval2  18323  istsr2  18519  isnsg2  19064  isnsg4  19075  isgim  19170  oppgid  19264  oppgcntz  19272  symgfix2  19322  efgval2  19630  iscyg2  19788  dmdprdd  19907  subgdmdprd  19942  issrg  20073  oppr1  20235  opprunit  20262  opprirred  20307  isrnghm  20326  isrhm  20363  issubrng  20432  subsubrng2  20449  subsubrg2  20484  rngcinv  20522  ringcinv  20556  isdomn2  20596  isdomn2OLD  20597  islmim  20945  lbsextg  21048  lidlnz  21128  resubdrg  21493  unocv  21565  pjfval2  21594  islinds2  21698  opsrtoslem1  21938  mdetunilem8  22482  istop2g  22759  isbasis2g  22811  tgval2  22819  isclo2  22951  isnrm2  23221  is1stc2  23305  llyi  23337  isfbas2  23698  elfg  23734  ufinffr  23792  isfcls  23872  alexsubALTlem2  23911  alexsubALTlem3  23912  cnextcn  23930  ustfilxp  24076  iscusp2  24165  metustid  24418  isclmp  24973  iscvsp  25004  tcphcph  25113  iscau3  25154  caucfil  25159  mdegleb  25945  ellogdm  26524  dvdsflsumcom  27074  logfac2  27104  dchrelbas3  27125  dchrvmasumlema  27387  nosupno  27591  noinfno  27606  noinfbnd1lem1  27611  dmscut  27699  made0  27761  mulsproplem5  27999  norecdiv  28069  elnnzs  28265  uzsind  28269  legtrid  28494  outpasch  28658  axcontlem5  28871  axcontlem6  28872  axcontlem7  28873  nb3grpr2  29286  iscplgr  29318  dfpth2  29632  pthdlem1  29669  wwlksnextinj  29802  usgr2wspthon  29868  rusgrnumwwlkl1  29871  isclwwlk  29886  clwwlkccatlem  29891  clwwlknon2x  30005  iseupthf1o  30104  frcond3  30171  frgr3v  30177  4cycl2vnunb  30192  frgrncvvdeqlem2  30202  fusgr2wsp2nb  30236  numclwlk1lem1  30271  hhcms  31105  isch3  31143  ocsh  31185  pjhtheu  31296  pjpreeq  31300  h1deoi  31451  h1dei  31452  eleigvec  31859  cvbr2  32185  cvnbtwn2  32189  cvnbtwn4  32191  mdsl2i  32224  cvmdi  32226  mdsymlem6  32310  cdj3lem3b  32342  mo5f  32391  nmo  32392  rexunirn  32394  dmrab  32399  difrab2  32400  disjunsn  32496  unipreima  32540  dfcnv2  32573  1stpreima  32603  isunit2  33164  lsmsnorb2  33336  prmidl0  33394  ssmxidl  33418  1arithufdlem4  33491  ressply1mon1p  33510  zarcls  33837  rhmpreimacnlem  33847  isrnsiga  34076  rossros  34143  omsmeas  34287  eulerpartlemr  34338  eulerpartlemgvv  34340  ballotlemodife  34462  plymulx  34512  signstfvneq0  34536  bnj251  34665  bnj252  34666  bnj257  34670  bnj290  34673  bnj1304  34782  bnj153  34843  bnj543  34856  bnj571  34869  bnj580  34876  bnj607  34879  bnj882  34889  bnj964  34906  bnj996  34919  bnj1033  34932  bnj1176  34968  bnj1186  34970  bnj1189  34972  bnj1204  34975  bnj1253  34980  bnj1452  35015  bnj1463  35018  dff15  35047  fineqvrep  35058  fineqvac  35060  lfuhgr3  35080  cusgredgex2  35083  usgrgt2cycl  35090  2cycl2d  35099  dfacycgr1  35104  erdszelem9  35159  cvmlift2lem9  35271  cvmlift2lem13  35275  satfvsucsuc  35325  satfdm  35329  satf0  35332  fmlasucdisj  35359  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  elmthm  35536  axinfprim  35666  axacprim  35667  xpab  35686  dfso2  35715  dford5reg  35743  dfon2lem5  35748  dfon2  35753  brtxp2  35842  brpprod3a  35847  dfom5b  35873  brcart  35893  brimg  35898  funpartlem  35903  dfrecs2  35911  cgrxfr  36016  segletr  36075  sumeq2si  36163  prodeq2si  36165  cbvprodvw2  36208  trer  36277  fneval  36313  neifg  36332  df3nandALT1  36360  andnand1  36362  nandsym1  36383  weiunlem2  36424  bj-eu3f  36802  bj-csbsnlem  36864  bj-snsetex  36924  bj-elsngl  36929  bj-snglc  36930  bj-restuni  37058  bj-dfmpoa  37079  bj-imdirco  37151  mptsnunlem  37299  icorempo  37312  isbasisrelowllem2  37317  relowlpssretop  37325  rdgeqoa  37331  difunieq  37335  dffinxpf  37346  nlpineqsn  37369  curf  37565  finixpnum  37572  ptrest  37586  poimirlem1  37588  poimirlem14  37601  poimirlem16  37603  poimirlem19  37606  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimir  37620  cnambfre  37635  itg2addnc  37641  ftc1anc  37668  opropabco  37691  isdrngo1  37923  keridl  37999  ispridlc  38037  selconj  38067  eldmres3  38238  eldmqsres  38248  cnvepres  38259  ecinn0  38308  alrmomorn  38313  moantr  38319  dfxrn2  38331  disjressuc2  38347  inxpxrn  38354  rnxrnres  38358  coss2cnvepres  38382  refrelredund4  38599  dferALTV2  38633  dfeldisj3  38684  dfpart2  38734  prtlem70  38823  prtlem100  38825  prtlem15  38841  islshpat  38983  lcvbr2  38988  lcvbr3  38989  lcvnbtwn2  38993  ellkr  39055  cvrval2  39240  cvrnbtwn2  39241  cvrnbtwn3  39242  cvrnbtwn4  39245  ishlat2  39319  lplnexatN  39530  islvol5  39546  dath  39703  pclfinclN  39917  lhpexle3  39979  4atex2  40044  4atex2-0bOLDN  40046  isltrn2N  40087  cdleme0nex  40257  cdleme22b  40308  cdlemg17pq  40639  cdlemg19  40651  cdlemg21  40653  cdlemg33d  40676  dibopelvalN  41110  dibopelval2  41112  dib1dim  41132  dicelval2N  41149  diclspsn  41161  lcdlss  41586  mapd1o  41615  3factsumint2  41983  3factsumint3  41984  3factsumint  41986  hashnexinj  42089  sticksstones16  42123  sticksstones21  42128  unitscyglem3  42158  supinf  42203  fimgmcyclem  42494  eu6w  42637  mzpcompact2lem  42712  fz1eqin  42730  rexrabdioph  42755  expdiophlem1  42983  dford4  42991  fnwe2lem2  43013  fgraphopab  43165  dflim6  43226  onsucf1olem  43232  onsucrn  43233  nnoeomeqom  43274  faosnf0.11b  43389  ifpidg  43453  rp-fakeinunass  43477  rp-isfinite6  43480  dfsucon  43485  elinintrab  43539  elnonrel  43547  elmapintab  43558  dfrtrcl5  43591  imaiun1  43613  coiun1  43614  rfovcnvf1od  43966  andi3or  43986  uneqsn  43987  ntrneicls00  44051  rr-groth  44261  ismnushort  44263  rr-grothshortbi  44265  2sbc5g  44378  pm14.12  44383  2sb5nd  44523  uun2221  44775  uun2221p1  44776  uun2221p2  44777  2sb5ndVD  44872  2sb5ndALT  44894  modelaxreplem3  44943  iindif2f  45127  disjinfi  45159  climuz  45715  dfxlim2  45819  cncfshift  45845  dvnmul  45914  dvnprodlem2  45918  ismbl3  45957  ismbl4  45964  stoweidlem26  45997  stoweidlem35  46006  fourierdlem54  46131  fourierdlem83  46160  fourierdlem100  46177  fourierdlem104  46181  fourierdlem109  46186  fourierdlem112  46189  smfpimcc  46779  fcoresf1ob  47047  f1cof1b  47051  f1ocof1ob  47055  2reu8i  47087  dfdfat2  47102  ffnaov  47173  an4com24  47242  4an21  47244  iccpartiltu  47396  prproropf1olem0  47476  dfgric2  47888  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgprismgr4cycllem10  48067  2zrngmmgm  48213  rngcinvALTV  48237  ringcinvALTV  48271  pgrpgt2nabl  48327  islindeps  48415  lindslinindsimp1  48419  lindslinindsimp2  48425  ldepslinc  48471  blen1b  48550  coxp  48794  i0oii  48881  io1ii  48882  isthinc2  49382  isthinc3  49383  isthincd2  49399  istermc2  49437  istermc3  49438  dffun3f  49644  setrec1lem3  49651  elpglem3  49675  elpg  49676