Theorem anbi2i 635

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1ci  638  anbi12i  640  bianass  655  an42  670  anandir  690  dfbi3  1065  dn1  1073  dfifp3  1081  ifpdfbiOLD  1087  4anpull2OLD  1383  an3andi  1513  an33rean  1514  anxordi  1556  cadcoma  1645  nic-mpALT  1705  nic-axALT  1707  3exdistr  1993  4exdistr  1994  19.27v  2028  19.27  2266  19.41  2274  2sb5  2315  dfsb7  2316  dfeumo  2566  mo4f  2597  eu3v  2600  eu6  2604  dfeu  2625  eu2  2639  eu4  2645  2mos  2679  2eu4  2684  r3ex  3206  ceqsex3v  3509  ceqsex4v  3510  ceqsex8v  3512  reu2  3690  reu6  3691  reu4  3696  reu7  3697  rmo3f  3699  rmo4f  3700  2reu5lem3  3722  2reu5  3723  sbcimdv  3814  sbcg  3818  rmo3  3843  reuan  3851  dfpss2  4043  difdif  4089  raldifb  4103  inass  4180  dfss4  4222  dfin2  4224  indi  4237  indifdi  4247  undif3  4253  difin0ss  4328  inssdif0OLD  4330  2nreu  4409  2reu4lem  4486  rexdifpr  4627  reuprg0  4670  ssdifsn  4758  ssunpr  4801  uniprg  4890  uniun  4897  uniinOLD  4899  csbuni  4905  dfiun2g  4996  iunin2  5037  iundif2  5040  iindif2  5045  iinin2  5046  elpwpw  5070  axrep1  5241  axrep4v  5245  axrep4  5246  axrep4OLD  5247  reusv2lem4  5374  eqvinop  5471  opcom  5486  fconstmpt  5725  opeliunxp  5730  opeliun2xp  5731  xpundi  5732  elvvv  5739  opelinxp  5743  xpiindi  5823  elcnv2  5865  cnvuni  5878  dmuni  5906  brres  5987  dmres  6013  elidinxp  6048  restidsing  6057  elima3  6071  asymref  6118  imainss  6153  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  mptpreima  6241  coundir  6251  resco  6253  coass  6269  relrelss  6277  opreu2reurex  6299  dfpo2  6301  frpoind  6347  ordtri3or  6397  dffun2  6550  dffun6  6551  dffun3  6552  dffun4  6553  dffun5  6554  dffun6f  6555  dffun7  6567  dffun8  6568  dffun9  6569  svrelfun  6612  fncnv  6613  imadif  6624  dfmpt3  6673  fcnvres  6759  fint  6761  fin  6762  dff12  6777  fores  6806  dff1o4  6833  eqfnfv3  7031  fndmin  7044  fniniseg  7059  unpreima  7062  ffnfvf  7119  fsn2  7136  tpres  7206  fconstfv  7217  dff13f  7258  dff14a  7273  dff14b  7274  dff15  7275  isocnv2  7338  f1opr  7475  eloprabga  7528  ffnov  7545  eqfnov  7548  foov  7594  uniuni  7767  tfindsg  7863  findsg  7900  funcnvuni  7935  opabex3d  7968  opabex3rd  7969  opabex3  7970  1stconst  8101  2ndconst  8102  frxp  8128  soxp  8131  xpord3lem  8151  suppvalbr  8166  suppofssd  8205  suppcoss  8209  mpoxopovel  8222  brtpos  8237  tpostpos  8248  dfsmo2  8340  dfrecs3  8365  rdglem1  8408  tz7.49  8438  brwitnlem  8498  oeeu  8595  naddasslem2  8688  brinxper  8730  erinxp  8795  mapsncnv  8897  cbvixp  8918  cbvixpv  8919  ixpin  8927  ixpiin  8928  mptelixpg  8939  elixpsn  8941  ixpsnf1o  8942  xpassen  9066  omxpenlem  9073  sbthcl  9094  sbthfilem  9189  wemapsolem  9519  dford2  9596  inf2  9599  zfinf  9615  ttrclselem2  9702  trcl  9704  frind  9729  frr3g  9735  iscard2  9978  leweon  10011  aceq1  10117  dfac3  10121  dfac4  10122  dfac5lem2  10124  dfac5  10128  kmlem3  10152  kmlem4  10153  kmlem14  10163  kmlem15  10164  dfackm  10166  infmap2  10216  fin23lem25  10323  zorn2lem7  10501  brdom6disj  10531  zfcndrep  10616  zfcndinf  10620  fpwwe  10648  axgroth4  10834  grothprim  10836  grothtsk  10837  nqpr  11016  addsrmo  11075  mulsrmo  11076  opelreal  11132  elnnz  12618  elznn0nn  12622  peano2uz2  12702  nnwos  12957  dflt2  13191  xmullem  13308  4fvwrd4  13695  preduz  13697  elfznelfzo  13821  fzind2  13836  fsuppmapnn0fiubex  14048  hashinfxadd  14441  hashgt23el  14481  hashfun  14494  fi1uzind  14564  brfi1uzind  14565  opfi1uzind  14568  cotr2g  15039  shftdm  15134  rexfiuz  15425  cbvsum  15772  cbvsumv  15773  mertenslem2  15964  mertens  15965  cbvprod  15992  cbvprodv  15993  prodeq1i  15995  prodmo  16015  iprodmul  16082  divalglem10  16484  ndvdssub  16491  bitsmod  16518  algcvgblem  16659  isprm2  16764  isprm4  16766  hashdvds  16858  infpn2  16997  hashbc0  17089  xpscf  17643  funcpropd  17983  isffth2  17999  eldmcoa  18146  setcinv  18171  xpccatid  18268  yonedainv  18361  ispos  18394  ispos2  18395  joinfval2  18452  meetfval2  18466  istsr2  18664  isnsg2  19268  isnsg4  19279  isgim  19378  oppgid  19472  oppgcntz  19480  symgfix2  19532  efgval2  19840  iscyg2  19998  dmdprdd  20117  subgdmdprd  20152  issrg  20316  oppr1  20480  opprunit  20507  opprirred  20552  isrnghm  20571  isrhm  20609  issubrng  20698  subsubrng2  20715  subsubrg2  20750  rngcinv  20788  ringcinv  20822  isdomn2  20862  islmim  21235  lbsextg  21338  lidlnz  21428  prmidl0  21530  resubdrg  21810  unocv  21882  pjfval2  21911  islinds2  22015  opsrtoslem1  22258  mdetunilem8  22828  istop2g  23105  isbasis2g  23157  tgval2  23165  isclo2  23297  isnrm2  23567  is1stc2  23651  llyi  23684  isfbas2  24045  elfg  24081  ufinffr  24139  isfcls  24219  alexsubALTlem2  24258  alexsubALTlem3  24259  cnextcn  24277  ustfilxp  24423  iscusp2  24511  metustid  24764  isclmp  25309  iscvsp  25340  tcphcph  25449  iscau3  25490  caucfil  25495  mdegleb  26274  plymulidp  26496  ellogdm  26857  dvdsflsumcom  27405  logfac2  27434  dchrelbas3  27455  dchrvmasumlema  27717  nosupno  27920  noinfno  27935  noinfbnd1lem1  27940  dmcuts  28037  made0  28109  mulsproplem5  28366  norecdiv  28436  elnnzs  28647  uzsind  28651  zsoring  28655  legtrid  28913  outpasch  29090  tgaaddcpbllem2  29206  tgaaddcpbllem3  29207  tgaltai  29274  axcontlem5  29375  axcontlem6  29376  axcontlem7  29377  lfuhgr3  29557  nb3grpr2  29793  iscplgr  29825  dfpth2  30143  pthdlem1  30181  wwlksnextinj  30317  usgr2wspthon  30386  rusgrnumwwlkl1  30389  isclwwlk  30404  clwwlkccatlem  30409  clwwlknon2x  30523  iseupthf1o  30626  frcond3  30693  frgr3v  30699  4cycl2vnunb  30714  frgrncvvdeqlem2  30724  fusgr2wsp2nb  30758  numclwlk1lem1  30793  hhcms  31628  isch3  31666  ocsh  31708  pjhtheu  31819  pjpreeq  31823  h1deoi  31974  h1dei  31975  eleigvec  32382  cvbr2  32708  cvnbtwn2  32712  cvnbtwn4  32714  mdsl2i  32747  cvmdi  32749  mdsymlem6  32833  cdj3lem3b  32865  mo5f  32908  nmo  32909  rexunirn  32911  dmrab  32916  difrab2  32917  disjunsn  33012  unipreima  33061  dfcnv2  33093  1stpreima  33125  isunit2  33625  lsmsnorb2  33771  ssmxidl  33823  1arithufdlem4  33903  ressply1mon1p  33924  extdgfialglem1  34148  zarcls  34330  rhmpreimacnlem  34340  isrnsiga  34569  rossros  34637  omsmeas  34780  eulerpartlemr  34831  eulerpartlemgvv  34833  ballotlemodife  34955  signstfvneq0  35026  bnj251  35158  bnj252  35159  bnj257  35163  bnj290  35166  bnj1304  35274  bnj153  35335  bnj543  35348  bnj571  35361  bnj580  35368  bnj607  35371  bnj882  35381  bnj964  35398  bnj996  35411  bnj1033  35424  bnj1176  35460  bnj1186  35462  bnj1189  35464  bnj1204  35467  bnj1253  35472  bnj1452  35507  bnj1463  35510  axprALT2  35563  fineqvrep  35586  fineqvac  35588  kardexen  35635  cusgredgex2  35667  usgrgt2cycl  35669  2cycl2d  35672  dfacycgr1  35675  erdszelem9  35730  cvmlift2lem9  35842  cvmlift2lem13  35846  satfvsucsuc  35896  satfdm  35900  satf0  35903  fmlasucdisj  35930  satffunlem  35932  satffunlem1lem1  35933  satffunlem2lem1  35935  elmthm  36107  axinfprim  36237  axacprim  36238  xpab  36257  dfso2  36286  dford5reg  36311  dfon2lem5  36316  dfon2  36321  brtxp2  36410  brpprod3a  36415  dfom5b  36441  brcart  36461  brimg  36466  funpartlem  36473  dfrecs2  36481  cgrxfr  36586  segletr  36645  sumeq2si  36773  prodeq2si  36775  cbvprodvw2  36818  trer  36886  fneval  36922  neifg  36941  df3nandALT1  36969  andnand1  36971  nandsym1  36992  weiunlem  37033  regsfromregtco  37108  mh-infprim2bi  37117  mh-infprim3bi  37118  bj-df-sb  37331  bj-dfsbc  37333  bj-eu3f  37535  bj-csbsnlem  37597  bj-snsetex  37658  bj-elsngl  37663  bj-snglc  37664  bj-restuni  37798  bj-dfmpoa  37819  bj-imdirco  37893  mptsnunlem  38043  icorempo  38056  isbasisrelowllem2  38061  relowlpssretop  38069  rdgeqoa  38075  difunieq  38079  dffinxpf  38090  nlpineqsn  38113  curf  38308  finixpnum  38315  ptrest  38329  poimirlem1  38331  poimirlem14  38344  poimirlem16  38346  poimirlem19  38349  poimirlem25  38355  poimirlem26  38356  poimirlem27  38357  poimir  38363  cnambfre  38378  itg2addnc  38384  ftc1anc  38411  opropabco  38435  isdrngo1  38667  keridl  38743  ispridlc  38781  selconj  38809  eldmres3  38992  eldmqsres  39002  cnvepres  39013  ecinn0  39062  alrmomorn  39067  moantr  39081  dfxrn2  39094  disjressuc2  39120  inxpxrn  39127  rnxrnres  39131  coss2cnvepres  39217  refrelredund4  39428  dferALTV2  39462  dfeldisj3  39520  dfpart2  39581  dfpeters2  39683  petseq  39685  prtlem70  39691  prtlem100  39693  prtlem15  39709  islshpat  39851  lcvbr2  39856  lcvbr3  39857  lcvnbtwn2  39861  ellkr  39923  cvrval2  40108  cvrnbtwn2  40109  cvrnbtwn3  40110  cvrnbtwn4  40113  ishlat2  40187  lplnexatN  40397  islvol5  40413  dath  40570  pclfinclN  40784  lhpexle3  40846  4atex2  40911  4atex2-0bOLDN  40913  isltrn2N  40954  cdleme0nex  41124  cdleme22b  41175  cdlemg17pq  41506  cdlemg19  41518  cdlemg21  41520  cdlemg33d  41543  dibopelvalN  41977  dibopelval2  41979  dib1dim  41999  dicelval2N  42016  diclspsn  42028  lcdlss  42453  mapd1o  42482  3factsumint2  42849  3factsumint3  42850  3factsumint  42852  hashnexinj  42955  sticksstones16  42989  sticksstones21  42994  unitscyglem3  43024  supinf  43070  fimgmcyclem  43361  eu6w  43468  mzpcompact2lem  43542  fz1eqin  43560  rexrabdioph  43581  expdiophlem1  43808  dford4  43816  fnwe2lem2  43838  fgraphopab  43990  dflim6  44051  onsucf1olem  44057  onsucrn  44058  nnoeomeqom  44099  faosnf0.11b  44213  ifpidg  44277  rp-fakeinunass  44301  rp-isfinite6  44304  dfsucon  44309  elinintrab  44363  elnonrel  44371  elmapintab  44382  dfrtrcl5  44415  imaiun1  44437  coiun1  44438  rfovcnvf1od  44790  andi3or  44810  uneqsn  44811  ntrneicls00  44875  rr-groth  45069  ismnushort  45071  rr-grothshortbi  45073  2sbc5g  45186  pm14.12  45191  2sb5nd  45329  uun2221  45581  uun2221p1  45582  uun2221p2  45583  2sb5ndVD  45678  2sb5ndALT  45700  modelaxreplem3  45749  iindif2f  45938  disjinfi  45970  climuz  46518  dfxlim2  46622  cncfshift  46648  dvnmul  46717  dvnprodlem2  46721  ismbl3  46760  ismbl4  46767  stoweidlem26  46800  stoweidlem35  46809  fourierdlem54  46934  fourierdlem83  46963  fourierdlem100  46980  fourierdlem104  46984  fourierdlem109  46989  fourierdlem112  46992  smfpimcc  47582  fcoresf1ob  47870  f1cof1b  47874  f1ocof1ob  47878  2reu8i  47910  dfdfat2  47925  ffnaov  47996  an4com24  48065  4an21  48067  iccpartiltu  48231  prproropf1olem0  48311  dfgric2  48740  gpgvtxedg0  48888  gpgvtxedg1  48889  gpgprismgr4cycllem10  48929  grlimedgnedg  48956  2zrngmmgm  49076  rngcinvALTV  49100  ringcinvALTV  49134  isprmrng  49160  pgrpgt2nabl  49205  islindeps  49292  lindslinindsimp1  49296  lindslinindsimp2  49302  ldepslinc  49348  blen1b  49427  coxp  49670  i0oii  49757  io1ii  49758  isthinc2  50257  isthinc3  50258  isthincd2  50274  istermc2  50312  istermc3  50313  dffun3f  50519  setrec1lem3  50526  elpglem3  50550  elpg  50551  alsanmo  50647  ralsanmo  50648  2alsraln0  50654  2alsraln0id  50655