Theorem anbi2i 624

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  627  anbi12i  629  bianass  643  an42  658  anandir  678  dfbi3  1050  dn1  1058  dfifp3  1066  ifpdfbi  1071  4anpull2  1363  an3andi  1485  an33rean  1486  anxordi  1528  cadcoma  1614  nic-mpALT  1674  nic-axALT  1676  3exdistr  1962  4exdistr  1963  19.27v  1997  19.27  2235  19.41  2243  2sb5  2285  dfsb7  2286  dfeumo  2536  mo4f  2567  eu3v  2570  eu6  2574  dfeu  2595  eu2  2609  eu4  2615  2mos  2649  2mosOLD  2650  2eu4  2655  r3ex  3176  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  reu2  3671  reu6  3672  reu4  3677  reu7  3678  rmo3f  3680  rmo4f  3681  2reu5lem3  3703  2reu5  3704  sbcimdv  3797  sbcg  3801  rmo3  3827  reuan  3834  dfpss2  4028  difdif  4075  raldifb  4089  inass  4168  dfss4  4209  dfin2  4211  indi  4224  indifdi  4234  undif3  4240  difin0ss  4313  inssdif0  4314  2nreu  4384  2reu4lem  4463  rexdifpr  4603  reuprg0  4646  ssdifsn  4733  ssunpr  4777  uniprg  4866  uniun  4873  uniin  4874  csbuni  4880  dfiun2g  4972  iunin2  5013  iundif2  5016  iindif2  5019  iinin2  5020  elpwpw  5044  axrep1  5213  axrep4v  5217  axrep4  5218  axrep4OLD  5219  reusv2lem4  5343  eqvinop  5440  opcom  5455  fconstmpt  5693  opeliunxp  5698  opeliun2xp  5699  xpundi  5700  elvvv  5707  opelinxp  5711  xpiindi  5790  elcnv2  5832  cnvuni  5841  dmuni  5869  brres  5951  dmres  5977  elidinxp  6009  restidsing  6018  elima3  6032  asymref  6079  imainss  6118  difxp  6128  xpdifid  6132  mptpreima  6202  coundir  6212  resco  6214  coass  6230  relrelss  6237  opreu2reurex  6258  dfpo2  6260  frpoind  6306  ordtri3or  6355  dffun2  6508  dffun6  6509  dffun3  6510  dffun4  6511  dffun5  6512  dffun6f  6513  dffun7  6525  dffun8  6526  dffun9  6527  svrelfun  6570  fncnv  6571  imadif  6582  dfmpt3  6632  fcnvres  6717  fint  6719  fin  6720  dff12  6735  fores  6762  dff1o4  6788  eqfnfv3  6985  fndmin  6997  fniniseg  7012  unpreima  7015  ffnfvf  7072  fsn2  7089  tpres  7156  fconstfv  7167  dff13f  7210  dff14a  7225  dff14b  7226  isocnv2  7286  f1opr  7423  eloprabga  7476  ffnov  7493  eqfnov  7496  foov  7541  uniuni  7716  tfindsg  7812  findsg  7848  funcnvuni  7883  opabex3d  7918  opabex3rd  7919  opabex3  7920  1stconst  8050  2ndconst  8051  frxp  8076  soxp  8079  xpord3lem  8099  suppvalbr  8114  suppofssd  8153  suppcoss  8157  mpoxopovel  8170  brtpos  8185  tpostpos  8196  dfsmo2  8287  dfrecs3  8312  rdglem1  8354  tz7.49  8384  brwitnlem  8442  oeeu  8539  naddasslem2  8631  brinxper  8673  erinxp  8738  mapsncnv  8841  cbvixp  8862  cbvixpv  8863  ixpin  8871  ixpiin  8872  mptelixpg  8883  elixpsn  8885  ixpsnf1o  8886  xpassen  9009  omxpenlem  9016  sbthcl  9037  sbthfilem  9132  wemapsolem  9465  dford2  9541  inf2  9544  zfinf  9560  ttrclselem2  9647  trcl  9649  frind  9674  frr3g  9680  iscard2  9900  leweon  9933  aceq1  10039  dfac3  10043  dfac4  10044  dfac5lem2  10046  dfac5  10051  kmlem3  10075  kmlem4  10076  kmlem14  10086  kmlem15  10087  dfackm  10089  infmap2  10139  fin23lem25  10246  zorn2lem7  10424  brdom6disj  10454  zfcndrep  10537  zfcndinf  10541  fpwwe  10569  axgroth4  10755  grothprim  10757  grothtsk  10758  nqpr  10937  addsrmo  10996  mulsrmo  10997  opelreal  11053  elnnz  12534  elznn0nn  12538  peano2uz2  12617  nnwos  12865  dflt2  13099  xmullem  13216  4fvwrd4  13602  preduz  13604  elfznelfzo  13728  fzind2  13743  fsuppmapnn0fiubex  13954  hashinfxadd  14347  hashgt23el  14386  hashfun  14399  fi1uzind  14469  brfi1uzind  14470  opfi1uzind  14473  cotr2g  14938  shftdm  15033  rexfiuz  15310  cbvsum  15657  cbvsumv  15658  mertenslem2  15850  mertens  15851  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  prodmo  15901  iprodmul  15968  divalglem10  16371  ndvdssub  16378  bitsmod  16405  algcvgblem  16546  isprm2  16651  isprm4  16653  hashdvds  16745  infpn2  16884  hashbc0  16976  xpscf  17529  funcpropd  17869  isffth2  17885  eldmcoa  18032  setcinv  18057  xpccatid  18154  yonedainv  18247  ispos  18280  ispos2  18281  joinfval2  18338  meetfval2  18352  istsr2  18550  isnsg2  19131  isnsg4  19142  isgim  19237  oppgid  19331  oppgcntz  19339  symgfix2  19391  efgval2  19699  iscyg2  19857  dmdprdd  19976  subgdmdprd  20011  issrg  20169  oppr1  20330  opprunit  20357  opprirred  20402  isrnghm  20421  isrhm  20458  issubrng  20524  subsubrng2  20541  subsubrg2  20576  rngcinv  20614  ringcinv  20648  isdomn2  20688  isdomn2OLD  20689  islmim  21057  lbsextg  21160  lidlnz  21240  resubdrg  21588  unocv  21660  pjfval2  21689  islinds2  21793  opsrtoslem1  22033  mdetunilem8  22584  istop2g  22861  isbasis2g  22913  tgval2  22921  isclo2  23053  isnrm2  23323  is1stc2  23407  llyi  23439  isfbas2  23800  elfg  23836  ufinffr  23894  isfcls  23974  alexsubALTlem2  24013  alexsubALTlem3  24014  cnextcn  24032  ustfilxp  24178  iscusp2  24266  metustid  24519  isclmp  25064  iscvsp  25095  tcphcph  25204  iscau3  25245  caucfil  25250  mdegleb  26029  ellogdm  26603  dvdsflsumcom  27151  logfac2  27180  dchrelbas3  27201  dchrvmasumlema  27463  nosupno  27667  noinfno  27682  noinfbnd1lem1  27687  dmcuts  27783  made0  27855  mulsproplem5  28112  norecdiv  28182  elnnzs  28393  uzsind  28397  zsoring  28401  legtrid  28659  outpasch  28823  axcontlem5  29037  axcontlem6  29038  axcontlem7  29039  nb3grpr2  29452  iscplgr  29484  dfpth2  29797  pthdlem1  29834  wwlksnextinj  29967  usgr2wspthon  30036  rusgrnumwwlkl1  30039  isclwwlk  30054  clwwlkccatlem  30059  clwwlknon2x  30173  iseupthf1o  30272  frcond3  30339  frgr3v  30345  4cycl2vnunb  30360  frgrncvvdeqlem2  30370  fusgr2wsp2nb  30404  numclwlk1lem1  30439  hhcms  31274  isch3  31312  ocsh  31354  pjhtheu  31465  pjpreeq  31469  h1deoi  31620  h1dei  31621  eleigvec  32028  cvbr2  32354  cvnbtwn2  32358  cvnbtwn4  32360  mdsl2i  32393  cvmdi  32395  mdsymlem6  32479  cdj3lem3b  32511  mo5f  32558  nmo  32559  rexunirn  32561  dmrab  32566  difrab2  32567  disjunsn  32664  unipreima  32716  dfcnv2  32748  1stpreima  32780  isunit2  33301  lsmsnorb2  33452  prmidl0  33510  ssmxidl  33534  1arithufdlem4  33607  ressply1mon1p  33628  extdgfialglem1  33836  zarcls  34018  rhmpreimacnlem  34028  isrnsiga  34257  rossros  34324  omsmeas  34467  eulerpartlemr  34518  eulerpartlemgvv  34520  ballotlemodife  34642  plymulx  34692  signstfvneq0  34716  bnj251  34845  bnj252  34846  bnj257  34850  bnj290  34853  bnj1304  34961  bnj153  35022  bnj543  35035  bnj571  35048  bnj580  35055  bnj607  35058  bnj882  35068  bnj964  35085  bnj996  35098  bnj1033  35111  bnj1176  35147  bnj1186  35149  bnj1189  35151  bnj1204  35154  bnj1253  35159  bnj1452  35194  bnj1463  35197  dff15  35227  axprALT2  35253  fineqvrep  35258  fineqvac  35260  lfuhgr3  35302  cusgredgex2  35305  usgrgt2cycl  35312  2cycl2d  35321  dfacycgr1  35326  erdszelem9  35381  cvmlift2lem9  35493  cvmlift2lem13  35497  satfvsucsuc  35547  satfdm  35551  satf0  35554  fmlasucdisj  35581  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  elmthm  35758  axinfprim  35888  axacprim  35889  xpab  35908  dfso2  35937  dford5reg  35962  dfon2lem5  35967  dfon2  35972  brtxp2  36061  brpprod3a  36066  dfom5b  36092  brcart  36112  brimg  36117  funpartlem  36124  dfrecs2  36132  cgrxfr  36237  segletr  36296  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  trer  36498  fneval  36534  neifg  36553  df3nandALT1  36581  andnand1  36583  nandsym1  36604  weiunlem  36645  regsfromregtco  36720  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-df-sb  36944  bj-dfsbc  36946  bj-eu3f  37148  bj-csbsnlem  37210  bj-snsetex  37270  bj-elsngl  37275  bj-snglc  37276  bj-restuni  37409  bj-dfmpoa  37430  bj-imdirco  37504  mptsnunlem  37654  icorempo  37667  isbasisrelowllem2  37672  relowlpssretop  37680  rdgeqoa  37686  difunieq  37690  dffinxpf  37701  nlpineqsn  37724  curf  37919  finixpnum  37926  ptrest  37940  poimirlem1  37942  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimir  37974  cnambfre  37989  itg2addnc  37995  ftc1anc  38022  opropabco  38045  isdrngo1  38277  keridl  38353  ispridlc  38391  selconj  38421  eldmres3  38604  eldmqsres  38614  cnvepres  38625  ecinn0  38674  alrmomorn  38679  moantr  38693  dfxrn2  38706  disjressuc2  38732  inxpxrn  38739  rnxrnres  38743  coss2cnvepres  38829  refrelredund4  39040  dferALTV2  39074  dfeldisj3  39132  dfpart2  39193  dfpeters2  39295  petseq  39297  prtlem70  39303  prtlem100  39305  prtlem15  39321  islshpat  39463  lcvbr2  39468  lcvbr3  39469  lcvnbtwn2  39473  ellkr  39535  cvrval2  39720  cvrnbtwn2  39721  cvrnbtwn3  39722  cvrnbtwn4  39725  ishlat2  39799  lplnexatN  40009  islvol5  40025  dath  40182  pclfinclN  40396  lhpexle3  40458  4atex2  40523  4atex2-0bOLDN  40525  isltrn2N  40566  cdleme0nex  40736  cdleme22b  40787  cdlemg17pq  41118  cdlemg19  41130  cdlemg21  41132  cdlemg33d  41155  dibopelvalN  41589  dibopelval2  41591  dib1dim  41611  dicelval2N  41628  diclspsn  41640  lcdlss  42065  mapd1o  42094  3factsumint2  42461  3factsumint3  42462  3factsumint  42464  hashnexinj  42567  sticksstones16  42601  sticksstones21  42606  unitscyglem3  42636  supinf  42681  fimgmcyclem  42978  eu6w  43109  mzpcompact2lem  43183  fz1eqin  43201  rexrabdioph  43222  expdiophlem1  43449  dford4  43457  fnwe2lem2  43479  fgraphopab  43631  dflim6  43692  onsucf1olem  43698  onsucrn  43699  nnoeomeqom  43740  faosnf0.11b  43854  ifpidg  43918  rp-fakeinunass  43942  rp-isfinite6  43945  dfsucon  43950  elinintrab  44004  elnonrel  44012  elmapintab  44023  dfrtrcl5  44056  imaiun1  44078  coiun1  44079  rfovcnvf1od  44431  andi3or  44451  uneqsn  44452  ntrneicls00  44516  rr-groth  44726  ismnushort  44728  rr-grothshortbi  44730  2sbc5g  44843  pm14.12  44848  2sb5nd  44987  uun2221  45239  uun2221p1  45240  uun2221p2  45241  2sb5ndVD  45336  2sb5ndALT  45358  modelaxreplem3  45407  iindif2f  45590  disjinfi  45622  climuz  46172  dfxlim2  46276  cncfshift  46302  dvnmul  46371  dvnprodlem2  46375  ismbl3  46414  ismbl4  46421  stoweidlem26  46454  stoweidlem35  46463  fourierdlem54  46588  fourierdlem83  46617  fourierdlem100  46634  fourierdlem104  46638  fourierdlem109  46643  fourierdlem112  46646  smfpimcc  47236  fcoresf1ob  47521  f1cof1b  47525  f1ocof1ob  47529  2reu8i  47561  dfdfat2  47576  ffnaov  47647  an4com24  47716  4an21  47718  iccpartiltu  47882  prproropf1olem0  47962  dfgric2  48391  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgprismgr4cycllem10  48580  grlimedgnedg  48607  2zrngmmgm  48728  rngcinvALTV  48752  ringcinvALTV  48786  pgrpgt2nabl  48842  islindeps  48929  lindslinindsimp1  48933  lindslinindsimp2  48939  ldepslinc  48985  blen1b  49064  coxp  49308  i0oii  49395  io1ii  49396  isthinc2  49895  isthinc3  49896  isthincd2  49912  istermc2  49950  istermc3  49951  dffun3f  50157  setrec1lem3  50164  elpglem3  50188  elpg  50189