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  2263  19.41  2271  2sb5  2311  dfsb7  2312  dfeumo  2561  mo4f  2592  eu3v  2595  eu6  2599  dfeu  2620  eu2  2634  eu4  2640  2mos  2674  2eu4  2679  r3ex  3201  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  reu2  3683  reu6  3684  reu4  3689  reu7  3690  rmo3f  3692  rmo4f  3693  2reu5lem3  3715  2reu5  3716  sbcimdv  3807  sbcg  3811  rmo3  3836  reuan  3844  dfpss2  4036  difdif  4082  raldifb  4096  inass  4173  dfss4  4215  dfin2  4217  indi  4230  indifdi  4240  undif3  4246  difin0ss  4321  inssdif0OLD  4323  2nreu  4402  2reu4lem  4479  rexdifpr  4620  reuprg0  4663  ssdifsn  4751  ssunpr  4794  uniprg  4883  uniun  4890  uniinOLD  4892  csbuni  4898  dfiun2g  4988  iunin2  5029  iundif2  5032  iindif2  5037  iinin2  5038  elpwpw  5062  axrep1  5233  axrep4v  5237  axrep4  5238  axrep4OLD  5239  reusv2lem4  5366  eqvinop  5463  opcom  5478  fconstmpt  5717  opeliunxp  5722  opeliun2xp  5723  xpundi  5724  elvvv  5731  opelinxp  5735  xpiindi  5815  elcnv2  5857  cnvuni  5870  dmuni  5898  brres  5979  dmres  6005  elidinxp  6040  restidsing  6049  elima3  6063  asymref  6110  imainss  6145  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  mptpreima  6234  coundir  6244  resco  6246  coass  6262  relrelss  6270  opreu2reurex  6292  dfpo2  6294  frpoind  6340  ordtri3or  6390  dffun2  6543  dffun6  6544  dffun3  6545  dffun4  6546  dffun5  6547  dffun6f  6548  dffun7  6561  dffun8  6562  dffun9  6563  svrelfun  6606  fncnv  6607  imadif  6618  dfmpt3  6667  fcnvres  6753  fint  6755  fin  6756  dff12  6771  fores  6800  dff1o4  6827  eqfnfv3  7025  fndmin  7038  fniniseg  7053  unpreima  7056  ffnfvf  7114  fsn2  7131  tpres  7201  fconstfv  7212  dff13f  7253  dff14a  7268  dff14b  7269  dff15  7270  isocnv2  7333  f1opr  7470  eloprabga  7523  ffnov  7540  eqfnov  7543  foov  7589  uniuni  7762  tfindsg  7858  findsg  7895  funcnvuni  7930  opabex3d  7963  opabex3rd  7964  opabex3  7965  1stconst  8098  2ndconst  8099  frxp  8125  soxp  8128  xpord3lem  8148  suppvalbr  8163  suppofssd  8202  suppcoss  8206  mpoxopovel  8219  brtpos  8234  tpostpos  8245  dfsmo2  8337  dfrecs3  8362  rdglem1  8405  tz7.49  8437  brwitnlem  8497  oeeu  8594  naddasslem2  8687  brinxper  8729  erinxp  8794  curf  8872  mapsncnv  8903  cbvixp  8924  cbvixpv  8925  ixpin  8933  ixpiin  8934  mptelixpg  8945  elixpsn  8947  ixpsnf1o  8948  xpassen  9072  omxpenlem  9079  sbthcl  9100  sbthfilem  9195  wemapsolem  9525  dford2  9602  inf2  9605  zfinf  9621  ttrclselem2  9708  trcl  9710  frind  9735  frr3g  9741  iscard2  9984  leweon  10017  aceq1  10123  dfac3  10127  dfac4  10128  dfac5lem2  10130  dfac5  10134  kmlem3  10158  kmlem4  10159  kmlem14  10169  kmlem15  10170  dfackm  10172  infmap2  10222  fin23lem25  10329  zorn2lem7  10507  brdom6disj  10538  zfcndrep  10626  zfcndinf  10630  fpwwe  10658  axgroth4  10844  grothprim  10846  grothtsk  10847  nqpr  11026  addsrmo  11085  mulsrmo  11086  opelreal  11142  elnnz  12628  elznn0nn  12632  peano2uz2  12712  nnwos  12967  dflt2  13202  xmullem  13319  4fvwrd4  13706  preduz  13708  elfznelfzo  13832  fzind2  13847  fsuppmapnn0fiubex  14059  hashinfxadd  14452  hashgt23el  14492  hashfun  14505  fi1uzind  14575  brfi1uzind  14576  opfi1uzind  14579  cotr2g  15052  shftdm  15147  rexfiuz  15438  cbvsum  15785  cbvsumv  15786  mertenslem2  15977  mertens  15978  cbvprod  16005  cbvprodv  16006  prodeq1i  16008  prodmo  16026  iprodmul  16093  divalglem10  16495  ndvdssub  16502  bitsmod  16529  algcvgblem  16670  isprm2  16775  isprm4  16777  hashdvds  16869  infpn2  17008  hashbc0  17100  xpscf  17654  funcpropd  17994  isffth2  18010  eldmcoa  18157  setcinv  18182  xpccatid  18279  yonedainv  18372  ispos  18405  ispos2  18406  joinfval2  18463  meetfval2  18477  istsr2  18675  isnsg2  19282  isnsg4  19293  isgim  19392  oppgid  19486  oppgcntz  19494  symgfix2  19546  efgval2  19854  iscyg2  20012  dmdprdd  20131  subgdmdprd  20166  issrg  20330  oppr1  20494  opprunit  20521  opprirred  20566  isrnghm  20585  isrhm  20623  issubrng  20712  subsubrng2  20729  subsubrg2  20764  rngcinv  20802  ringcinv  20836  isdomn2  20876  islmim  21249  lbsextg  21352  lidlnz  21442  prmidl0  21544  resubdrg  21824  unocv  21896  pjfval2  21925  islinds2  22029  opsrtoslem1  22274  mdetunilem8  22844  istop2g  23124  isbasis2g  23176  tgval2  23184  isclo2  23316  isnrm2  23586  is1stc2  23670  llyi  23703  isfbas2  24064  elfg  24100  ufinffr  24158  isfcls  24238  alexsubALTlem2  24277  alexsubALTlem3  24278  cnextcn  24296  ustfilxp  24442  iscusp2  24530  metustid  24783  isclmp  25328  iscvsp  25359  tcphcph  25468  iscau3  25509  caucfil  25514  mdegleb  26292  plymulidp  26515  ellogdm  26879  dvdsflsumcom  27427  logfac2  27456  dchrelbas3  27477  dchrvmasumlema  27739  nosupno  27942  noinfno  27957  noinfbnd1lem1  27962  dmcuts  28059  made0  28131  mulsproplem5  28388  norecdiv  28458  elnnzs  28669  uzsind  28673  zsoring  28677  legtrid  28936  outpasch  29115  tgaaddcpbllem2  29232  tgaaddcpbllem3  29233  tgaltai  29327  axcontlem5  29428  axcontlem6  29429  axcontlem7  29430  lfuhgr3  29610  nb3grpr2  29846  iscplgr  29878  dfpth2  30196  pthdlem1  30234  wwlksnextinj  30370  usgr2wspthon  30439  rusgrnumwwlkl1  30442  isclwwlk  30457  clwwlkccatlem  30462  clwwlknon2x  30576  dfacycgr1  30632  iseupthf1o  30685  frcond3  30752  frgr3v  30758  4cycl2vnunb  30773  frgrncvvdeqlem2  30783  fusgr2wsp2nb  30817  numclwlk1lem1  30852  hhcms  31687  isch3  31725  ocsh  31767  pjhtheu  31878  pjpreeq  31882  h1deoi  32033  h1dei  32034  eleigvec  32441  cvbr2  32767  cvnbtwn2  32771  cvnbtwn4  32773  mdsl2i  32806  cvmdi  32808  mdsymlem6  32892  cdj3lem3b  32924  mo5f  32967  nmo  32968  rexunirn  32970  dmrab  32975  difrab2  32976  disjunsn  33070  unipreima  33119  dfcnv2  33151  1stpreima  33182  isunit2  33682  lsmsnorb2  33828  ssmxidl  33880  1arithufdlem4  33960  ressply1mon1p  33981  extdgfialglem1  34205  zarcls  34387  rhmpreimacnlem  34397  isrnsiga  34626  rossros  34694  omsmeas  34837  eulerpartlemr  34888  eulerpartlemgvv  34890  ballotlemodife  35012  signstfvneq0  35083  bnj251  35215  bnj252  35216  bnj257  35220  bnj290  35223  bnj1304  35331  bnj153  35392  bnj543  35405  bnj571  35418  bnj580  35425  bnj607  35428  bnj882  35438  bnj964  35455  bnj996  35468  bnj1033  35481  bnj1176  35517  bnj1186  35519  bnj1189  35521  bnj1204  35524  bnj1253  35529  bnj1452  35564  bnj1463  35567  axprALT2  35620  fineqvrep  35643  fineqvac  35645  kardexen  35692  cusgredgex2  35724  usgrgt2cycl  35726  2cycl2d  35729  erdszelem9  35781  cvmlift2lem9  35893  cvmlift2lem13  35897  satfvsucsuc  35947  satfdm  35951  satf0  35954  fmlasucdisj  35981  satffunlem  35983  satffunlem1lem1  35984  satffunlem2lem1  35986  elmthm  36158  axinfprim  36288  axacprim  36289  xpab  36308  dfso2  36337  dford5reg  36362  dfon2lem5  36367  dfon2  36372  brtxp2  36461  brpprod3a  36466  dfom5b  36492  brcart  36512  brimg  36517  funpartlem  36524  dfrecs2  36532  cgrxfr  36638  segletr  36697  sumeq2si  36825  prodeq2si  36827  cbvprodvw2  36870  trer  36938  fneval  36974  neifg  36993  df3nandALT1  37021  andnand1  37023  nandsym1  37044  weiunlem  37085  regsfromregtco  37160  mh-infprim2bi  37169  mh-infprim3bi  37170  bj-df-sb  37383  bj-dfsbc  37385  bj-eu3f  37587  bj-csbsnlem  37649  bj-snsetex  37710  bj-elsngl  37715  bj-snglc  37716  bj-restuni  37850  bj-dfmpoa  37871  bj-imdirco  37945  mptsnunlem  38095  icorempo  38108  isbasisrelowllem2  38113  relowlpssretop  38121  rdgeqoa  38127  difunieq  38131  dffinxpf  38142  nlpineqsn  38165  finixpnum  38362  ptrest  38371  poimirlem1  38373  poimirlem14  38386  poimirlem16  38388  poimirlem19  38391  poimirlem25  38397  poimirlem26  38398  poimirlem27  38399  poimir  38405  cnambfre  38420  itg2addnc  38426  ftc1anc  38453  opropabco  38477  isdrngo1  38709  keridl  38785  ispridlc  38823  selconj  38851  eldmres3  39034  eldmqsres  39044  cnvepres  39055  ecinn0  39104  alrmomorn  39109  moantr  39123  dfxrn2  39136  disjressuc2  39162  inxpxrn  39169  rnxrnres  39173  coss2cnvepres  39259  refrelredund4  39470  dferALTV2  39504  dfeldisj3  39562  dfpart2  39623  dfpeters2  39725  petseq  39727  prtlem70  39733  prtlem100  39735  prtlem15  39751  islshpat  39893  lcvbr2  39898  lcvbr3  39899  lcvnbtwn2  39903  ellkr  39965  cvrval2  40150  cvrnbtwn2  40151  cvrnbtwn3  40152  cvrnbtwn4  40155  ishlat2  40229  lplnexatN  40439  islvol5  40455  dath  40612  pclfinclN  40826  lhpexle3  40888  4atex2  40953  4atex2-0bOLDN  40955  isltrn2N  40996  cdleme0nex  41166  cdleme22b  41217  cdlemg17pq  41548  cdlemg19  41560  cdlemg21  41562  cdlemg33d  41585  dibopelvalN  42019  dibopelval2  42021  dib1dim  42041  dicelval2N  42058  diclspsn  42070  lcdlss  42495  mapd1o  42524  3factsumint2  42891  3factsumint3  42892  3factsumint  42894  hashnexinj  42997  sticksstones16  43031  sticksstones21  43036  unitscyglem3  43066  supinf  43112  fimgmcyclem  43418  eu6w  43525  mzpcompact2lem  43599  fz1eqin  43617  rexrabdioph  43638  expdiophlem1  43865  dford4  43873  fnwe2lem2  43895  fgraphopab  44047  dflim6  44108  onsucf1olem  44114  onsucrn  44115  nnoeomeqom  44156  faosnf0.11b  44270  ifpidg  44334  rp-fakeinunass  44358  rp-isfinite6  44361  dfsucon  44366  elinintrab  44420  elnonrel  44428  elmapintab  44439  dfrtrcl5  44472  imaiun1  44494  coiun1  44495  rfovcnvf1od  44847  andi3or  44867  uneqsn  44868  ntrneicls00  44932  rr-groth  45126  ismnushort  45128  rr-grothshortbi  45130  2sbc5g  45243  pm14.12  45248  2sb5nd  45386  uun2221  45638  uun2221p1  45639  uun2221p2  45640  2sb5ndVD  45735  2sb5ndALT  45757  modelaxreplem3  45806  iindif2f  45995  disjinfi  46027  climuz  46575  dfxlim2  46679  cncfshift  46705  dvnmul  46774  dvnprodlem2  46778  ismbl3  46817  ismbl4  46824  stoweidlem26  46857  stoweidlem35  46866  fourierdlem54  46991  fourierdlem83  47020  fourierdlem100  47037  fourierdlem104  47041  fourierdlem109  47046  fourierdlem112  47049  smfpimcc  47639  fcoresf1ob  47964  f1cof1b  47968  f1ocof1ob  47972  2reu8i  48004  dfdfat2  48019  ffnaov  48090  an4com24  48159  4an21  48161  iccpartiltu  48325  prproropf1olem0  48405  dfgric2  48834  gpgvtxedg0  48982  gpgvtxedg1  48983  gpgprismgr4cycllem10  49023  grlimedgnedg  49050  2zrngmmgm  49170  rngcinvALTV  49194  ringcinvALTV  49228  isprmrng  49254  pgrpgt2nabl  49299  islindeps  49386  lindslinindsimp1  49390  lindslinindsimp2  49396  ldepslinc  49442  blen1b  49521  coxp  49764  i0oii  49849  io1ii  49850  isthinc2  50349  isthinc3  50350  isthincd2  50366  istermc2  50404  istermc3  50405  dffun3f  50611  setrec1lem3  50618  elpglem3  50642  elpg  50643  alsanmo  50742  ralsanmo  50743  2alsraln0  50749  2alsraln0id  50750