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  2537  mo4f  2568  eu3v  2571  eu6  2575  dfeu  2596  eu2  2610  eu4  2616  2mos  2650  2mosOLD  2651  2eu4  2656  r3ex  3176  ceqsex3v  3496  ceqsex4v  3497  ceqsex8v  3499  reu2  3684  reu6  3685  reu4  3690  reu7  3691  rmo3f  3693  rmo4f  3694  2reu5lem3  3716  2reu5  3717  sbcimdv  3810  sbcg  3814  rmo3  3840  reuan  3847  dfpss2  4041  difdif  4088  raldifb  4102  inass  4181  dfss4  4222  dfin2  4224  indi  4237  indifdi  4247  undif3  4253  difin0ss  4326  inssdif0  4327  2nreu  4397  2reu4lem  4477  rexdifpr  4617  reuprg0  4660  ssdifsn  4745  ssunpr  4791  uniprg  4880  uniun  4887  uniin  4888  csbuni  4894  dfiun2g  4986  iunin2  5027  iundif2  5030  iindif2  5033  iinin2  5034  elpwpw  5058  axrep1  5226  axrep4v  5230  axrep4  5231  axrep4OLD  5232  reusv2lem4  5347  eqvinop  5436  opcom  5450  fconstmpt  5687  opeliunxp  5692  opeliun2xp  5693  xpundi  5694  elvvv  5701  opelinxp  5705  xpiindi  5785  elcnv2  5827  cnvuni  5836  dmuni  5864  brres  5946  dmres  5972  elidinxp  6004  restidsing  6013  elima3  6027  asymref  6074  imainss  6113  difxp  6123  xpdifid  6127  mptpreima  6197  coundir  6207  resco  6209  coass  6225  relrelss  6232  opreu2reurex  6253  dfpo2  6255  frpoind  6301  ordtri3or  6350  dffun2  6503  dffun6  6504  dffun3  6505  dffun4  6506  dffun5  6507  dffun6f  6508  dffun7  6520  dffun8  6521  dffun9  6522  svrelfun  6565  fncnv  6566  imadif  6577  dfmpt3  6627  fcnvres  6712  fint  6714  fin  6715  dff12  6730  fores  6757  dff1o4  6783  eqfnfv3  6980  fndmin  6992  fniniseg  7007  unpreima  7010  ffnfvf  7067  fsn2  7083  tpres  7149  fconstfv  7160  dff13f  7203  dff14a  7218  dff14b  7219  isocnv2  7279  f1opr  7416  eloprabga  7469  ffnov  7486  eqfnov  7489  foov  7534  uniuni  7709  tfindsg  7805  findsg  7841  funcnvuni  7876  opabex3d  7911  opabex3rd  7912  opabex3  7913  1stconst  8044  2ndconst  8045  frxp  8070  soxp  8073  xpord3lem  8093  suppvalbr  8108  suppofssd  8147  suppcoss  8151  mpoxopovel  8164  brtpos  8179  tpostpos  8190  dfsmo2  8281  dfrecs3  8306  rdglem1  8348  tz7.49  8378  brwitnlem  8436  oeeu  8533  naddasslem2  8625  brinxper  8667  erinxp  8732  mapsncnv  8835  cbvixp  8856  cbvixpv  8857  ixpin  8865  ixpiin  8866  mptelixpg  8877  elixpsn  8879  ixpsnf1o  8880  xpassen  9003  omxpenlem  9010  sbthcl  9031  sbthfilem  9126  wemapsolem  9459  dford2  9533  inf2  9536  zfinf  9552  ttrclselem2  9639  trcl  9641  frind  9666  frr3g  9672  iscard2  9892  leweon  9925  aceq1  10031  dfac3  10035  dfac4  10036  dfac5lem2  10038  dfac5  10043  kmlem3  10067  kmlem4  10068  kmlem14  10078  kmlem15  10079  dfackm  10081  infmap2  10131  fin23lem25  10238  zorn2lem7  10416  brdom6disj  10446  zfcndrep  10529  zfcndinf  10533  fpwwe  10561  axgroth4  10747  grothprim  10749  grothtsk  10750  nqpr  10929  addsrmo  10988  mulsrmo  10989  opelreal  11045  elnnz  12502  elznn0nn  12506  peano2uz2  12584  nnwos  12832  dflt2  13066  xmullem  13183  4fvwrd4  13568  preduz  13570  elfznelfzo  13693  fzind2  13708  fsuppmapnn0fiubex  13919  hashinfxadd  14312  hashgt23el  14351  hashfun  14364  fi1uzind  14434  brfi1uzind  14435  opfi1uzind  14438  cotr2g  14903  shftdm  14998  rexfiuz  15275  cbvsum  15622  cbvsumv  15623  mertenslem2  15812  mertens  15813  cbvprod  15840  cbvprodv  15841  prodeq1i  15843  prodmo  15863  iprodmul  15930  divalglem10  16333  ndvdssub  16340  bitsmod  16367  algcvgblem  16508  isprm2  16613  isprm4  16615  hashdvds  16706  infpn2  16845  hashbc0  16937  xpscf  17490  funcpropd  17830  isffth2  17846  eldmcoa  17993  setcinv  18018  xpccatid  18115  yonedainv  18208  ispos  18241  ispos2  18242  joinfval2  18299  meetfval2  18313  istsr2  18511  isnsg2  19089  isnsg4  19100  isgim  19195  oppgid  19289  oppgcntz  19297  symgfix2  19349  efgval2  19657  iscyg2  19815  dmdprdd  19934  subgdmdprd  19969  issrg  20127  oppr1  20290  opprunit  20317  opprirred  20362  isrnghm  20381  isrhm  20418  issubrng  20484  subsubrng2  20501  subsubrg2  20536  rngcinv  20574  ringcinv  20608  isdomn2  20648  isdomn2OLD  20649  islmim  21018  lbsextg  21121  lidlnz  21201  resubdrg  21567  unocv  21639  pjfval2  21668  islinds2  21772  opsrtoslem1  22014  mdetunilem8  22567  istop2g  22844  isbasis2g  22896  tgval2  22904  isclo2  23036  isnrm2  23306  is1stc2  23390  llyi  23422  isfbas2  23783  elfg  23819  ufinffr  23877  isfcls  23957  alexsubALTlem2  23996  alexsubALTlem3  23997  cnextcn  24015  ustfilxp  24161  iscusp2  24249  metustid  24502  isclmp  25057  iscvsp  25088  tcphcph  25197  iscau3  25238  caucfil  25243  mdegleb  26029  ellogdm  26608  dvdsflsumcom  27158  logfac2  27188  dchrelbas3  27209  dchrvmasumlema  27471  nosupno  27675  noinfno  27690  noinfbnd1lem1  27695  dmscut  27789  made0  27855  mulsproplem5  28102  norecdiv  28172  elnnzs  28380  uzsind  28384  zsoring  28388  legtrid  28646  outpasch  28810  axcontlem5  29024  axcontlem6  29025  axcontlem7  29026  nb3grpr2  29439  iscplgr  29471  dfpth2  29785  pthdlem1  29822  wwlksnextinj  29955  usgr2wspthon  30024  rusgrnumwwlkl1  30027  isclwwlk  30042  clwwlkccatlem  30047  clwwlknon2x  30161  iseupthf1o  30260  frcond3  30327  frgr3v  30333  4cycl2vnunb  30348  frgrncvvdeqlem2  30358  fusgr2wsp2nb  30392  numclwlk1lem1  30427  hhcms  31261  isch3  31299  ocsh  31341  pjhtheu  31452  pjpreeq  31456  h1deoi  31607  h1dei  31608  eleigvec  32015  cvbr2  32341  cvnbtwn2  32345  cvnbtwn4  32347  mdsl2i  32380  cvmdi  32382  mdsymlem6  32466  cdj3lem3b  32498  mo5f  32545  nmo  32546  rexunirn  32548  dmrab  32553  difrab2  32554  disjunsn  32651  unipreima  32703  dfcnv2  32735  1stpreima  32767  isunit2  33303  lsmsnorb2  33454  prmidl0  33512  ssmxidl  33536  1arithufdlem4  33609  ressply1mon1p  33630  extdgfialglem1  33830  zarcls  34012  rhmpreimacnlem  34022  isrnsiga  34251  rossros  34318  omsmeas  34461  eulerpartlemr  34512  eulerpartlemgvv  34514  ballotlemodife  34636  plymulx  34686  signstfvneq0  34710  bnj251  34839  bnj252  34840  bnj257  34844  bnj290  34847  bnj1304  34956  bnj153  35017  bnj543  35030  bnj571  35043  bnj580  35050  bnj607  35053  bnj882  35063  bnj964  35080  bnj996  35093  bnj1033  35106  bnj1176  35142  bnj1186  35144  bnj1189  35146  bnj1204  35149  bnj1253  35154  bnj1452  35189  bnj1463  35192  dff15  35221  fineqvrep  35251  fineqvac  35253  lfuhgr3  35295  cusgredgex2  35298  usgrgt2cycl  35305  2cycl2d  35314  dfacycgr1  35319  erdszelem9  35374  cvmlift2lem9  35486  cvmlift2lem13  35490  satfvsucsuc  35540  satfdm  35544  satf0  35547  fmlasucdisj  35574  satffunlem  35576  satffunlem1lem1  35577  satffunlem2lem1  35579  elmthm  35751  axinfprim  35881  axacprim  35882  xpab  35901  dfso2  35930  dford5reg  35955  dfon2lem5  35960  dfon2  35965  brtxp2  36054  brpprod3a  36059  dfom5b  36085  brcart  36105  brimg  36110  funpartlem  36117  dfrecs2  36125  cgrxfr  36230  segletr  36289  sumeq2si  36377  prodeq2si  36379  cbvprodvw2  36422  trer  36491  fneval  36527  neifg  36546  df3nandALT1  36574  andnand1  36576  nandsym1  36597  weiunlem2  36638  bj-df-sb  36828  bj-eu3f  37017  bj-csbsnlem  37079  bj-snsetex  37139  bj-elsngl  37144  bj-snglc  37145  bj-restuni  37273  bj-dfmpoa  37294  bj-imdirco  37366  mptsnunlem  37514  icorempo  37527  isbasisrelowllem2  37532  relowlpssretop  37540  rdgeqoa  37546  difunieq  37550  dffinxpf  37561  nlpineqsn  37584  curf  37770  finixpnum  37777  ptrest  37791  poimirlem1  37793  poimirlem14  37806  poimirlem16  37808  poimirlem19  37811  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimir  37825  cnambfre  37840  itg2addnc  37846  ftc1anc  37873  opropabco  37896  isdrngo1  38128  keridl  38204  ispridlc  38242  selconj  38272  eldmres3  38455  eldmqsres  38465  cnvepres  38476  ecinn0  38525  alrmomorn  38530  moantr  38544  dfxrn2  38557  disjressuc2  38583  inxpxrn  38590  rnxrnres  38594  coss2cnvepres  38680  refrelredund4  38891  dferALTV2  38925  dfeldisj3  38983  dfpart2  39044  dfpeters2  39146  petseq  39148  prtlem70  39154  prtlem100  39156  prtlem15  39172  islshpat  39314  lcvbr2  39319  lcvbr3  39320  lcvnbtwn2  39324  ellkr  39386  cvrval2  39571  cvrnbtwn2  39572  cvrnbtwn3  39573  cvrnbtwn4  39576  ishlat2  39650  lplnexatN  39860  islvol5  39876  dath  40033  pclfinclN  40247  lhpexle3  40309  4atex2  40374  4atex2-0bOLDN  40376  isltrn2N  40417  cdleme0nex  40587  cdleme22b  40638  cdlemg17pq  40969  cdlemg19  40981  cdlemg21  40983  cdlemg33d  41006  dibopelvalN  41440  dibopelval2  41442  dib1dim  41462  dicelval2N  41479  diclspsn  41491  lcdlss  41916  mapd1o  41945  3factsumint2  42313  3factsumint3  42314  3factsumint  42316  hashnexinj  42419  sticksstones16  42453  sticksstones21  42458  unitscyglem3  42488  supinf  42533  fimgmcyclem  42824  eu6w  42955  mzpcompact2lem  43029  fz1eqin  43047  rexrabdioph  43072  expdiophlem1  43299  dford4  43307  fnwe2lem2  43329  fgraphopab  43481  dflim6  43542  onsucf1olem  43548  onsucrn  43549  nnoeomeqom  43590  faosnf0.11b  43704  ifpidg  43768  rp-fakeinunass  43792  rp-isfinite6  43795  dfsucon  43800  elinintrab  43854  elnonrel  43862  elmapintab  43873  dfrtrcl5  43906  imaiun1  43928  coiun1  43929  rfovcnvf1od  44281  andi3or  44301  uneqsn  44302  ntrneicls00  44366  rr-groth  44576  ismnushort  44578  rr-grothshortbi  44580  2sbc5g  44693  pm14.12  44698  2sb5nd  44837  uun2221  45089  uun2221p1  45090  uun2221p2  45091  2sb5ndVD  45186  2sb5ndALT  45208  modelaxreplem3  45257  iindif2f  45440  disjinfi  45472  climuz  46024  dfxlim2  46128  cncfshift  46154  dvnmul  46223  dvnprodlem2  46227  ismbl3  46266  ismbl4  46273  stoweidlem26  46306  stoweidlem35  46315  fourierdlem54  46440  fourierdlem83  46469  fourierdlem100  46486  fourierdlem104  46490  fourierdlem109  46495  fourierdlem112  46498  smfpimcc  47088  fcoresf1ob  47355  f1cof1b  47359  f1ocof1ob  47363  2reu8i  47395  dfdfat2  47410  ffnaov  47481  an4com24  47550  4an21  47552  iccpartiltu  47704  prproropf1olem0  47784  dfgric2  48197  gpgvtxedg0  48345  gpgvtxedg1  48346  gpgprismgr4cycllem10  48386  grlimedgnedg  48413  2zrngmmgm  48534  rngcinvALTV  48558  ringcinvALTV  48592  pgrpgt2nabl  48648  islindeps  48735  lindslinindsimp1  48739  lindslinindsimp2  48745  ldepslinc  48791  blen1b  48870  coxp  49114  i0oii  49201  io1ii  49202  isthinc2  49701  isthinc3  49702  isthincd2  49718  istermc2  49756  istermc3  49757  dffun3f  49963  setrec1lem3  49970  elpglem3  49994  elpg  49995