Theorem anbi2i 634

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi1ci  637  anbi12i  639  bianass  654  an42  669  anandir  689  dfbi3  1063  dn1  1071  dfifp3  1079  ifpdfbiOLD  1085  4anpull2OLD  1381  an3andi  1510  an33rean  1511  anxordi  1553  cadcoma  1639  nic-mpALT  1699  nic-axALT  1701  3exdistr  1987  4exdistr  1988  19.27v  2022  19.27  2269  19.41  2277  2sb5  2319  dfsb7  2320  dfeumo  2570  mo4f  2601  eu3v  2604  eu6  2608  dfeu  2629  eu2  2643  eu4  2649  2mos  2683  2eu4  2688  r3ex  3210  ceqsex3v  3515  ceqsex4v  3516  ceqsex8v  3518  reu2  3697  reu6  3698  reu4  3703  reu7  3704  rmo3f  3706  rmo4f  3707  2reu5lem3  3729  2reu5  3730  sbcimdv  3821  sbcg  3825  rmo3  3851  reuan  3858  dfpss2  4050  difdif  4097  raldifb  4111  inass  4188  dfss4  4230  dfin2  4232  indi  4245  indifdi  4255  undif3  4261  difin0ss  4336  inssdif0  4337  2nreu  4415  2reu4lem  4489  rexdifpr  4630  reuprg0  4673  ssdifsn  4760  ssunpr  4803  uniprg  4892  uniun  4899  uniinOLD  4901  csbuni  4907  dfiun2g  4998  iunin2  5039  iundif2  5042  iindif2  5047  iinin2  5048  elpwpw  5072  axrep1  5243  axrep4v  5247  axrep4  5248  axrep4OLD  5249  reusv2lem4  5373  eqvinop  5470  opcom  5485  fconstmpt  5724  opeliunxp  5729  opeliun2xp  5730  xpundi  5731  elvvv  5738  opelinxp  5742  xpiindi  5822  elcnv2  5864  cnvuni  5877  dmuni  5905  brres  5986  dmres  6012  elidinxp  6047  restidsing  6056  elima3  6070  asymref  6117  imainss  6152  difxp  6162  xpdifid  6166  xpdifcnvepel  6167  mptpreima  6240  coundir  6250  resco  6252  coass  6268  relrelss  6275  opreu2reurex  6296  dfpo2  6298  frpoind  6344  ordtri3or  6394  dffun2  6547  dffun6  6548  dffun3  6549  dffun4  6550  dffun5  6551  dffun6f  6552  dffun7  6564  dffun8  6565  dffun9  6566  svrelfun  6609  fncnv  6610  imadif  6621  dfmpt3  6670  fcnvres  6756  fint  6758  fin  6759  dff12  6774  fores  6803  dff1o4  6830  eqfnfv3  7028  fndmin  7041  fniniseg  7056  unpreima  7059  ffnfvf  7116  fsn2  7133  tpres  7200  fconstfv  7211  dff13f  7254  dff14a  7269  dff14b  7270  isocnv2  7330  f1opr  7467  eloprabga  7520  ffnov  7537  eqfnov  7540  foov  7585  uniuni  7761  tfindsg  7857  findsg  7894  funcnvuni  7929  opabex3d  7962  opabex3rd  7963  opabex3  7964  1stconst  8095  2ndconst  8096  frxp  8122  soxp  8125  xpord3lem  8145  suppvalbr  8160  suppofssd  8199  suppcoss  8203  mpoxopovel  8216  brtpos  8231  tpostpos  8242  dfsmo2  8334  dfrecs3  8359  rdglem1  8402  tz7.49  8432  brwitnlem  8492  oeeu  8589  naddasslem2  8682  brinxper  8724  erinxp  8789  mapsncnv  8891  cbvixp  8912  cbvixpv  8913  ixpin  8921  ixpiin  8922  mptelixpg  8933  elixpsn  8935  ixpsnf1o  8936  xpassen  9059  omxpenlem  9066  sbthcl  9087  sbthfilem  9182  wemapsolem  9512  dford2  9589  inf2  9592  zfinf  9608  ttrclselem2  9695  trcl  9697  frind  9722  frr3g  9728  iscard2  9962  leweon  9995  aceq1  10101  dfac3  10105  dfac4  10106  dfac5lem2  10108  dfac5  10112  kmlem3  10136  kmlem4  10137  kmlem14  10147  kmlem15  10148  dfackm  10150  infmap2  10200  fin23lem25  10308  zorn2lem7  10486  brdom6disj  10516  zfcndrep  10599  zfcndinf  10603  fpwwe  10631  axgroth4  10817  grothprim  10819  grothtsk  10820  nqpr  10999  addsrmo  11058  mulsrmo  11059  opelreal  11115  elnnz  12601  elznn0nn  12605  peano2uz2  12684  nnwos  12939  dflt2  13173  xmullem  13290  4fvwrd4  13676  preduz  13678  elfznelfzo  13802  fzind2  13817  fsuppmapnn0fiubex  14028  hashinfxadd  14421  hashgt23el  14461  hashfun  14474  fi1uzind  14544  brfi1uzind  14545  opfi1uzind  14548  cotr2g  15013  shftdm  15108  rexfiuz  15399  cbvsum  15746  cbvsumv  15747  mertenslem2  15939  mertens  15940  cbvprod  15967  cbvprodv  15968  prodeq1i  15970  prodmo  15990  iprodmul  16057  divalglem10  16460  ndvdssub  16467  bitsmod  16494  algcvgblem  16635  isprm2  16740  isprm4  16742  hashdvds  16834  infpn2  16973  hashbc0  17065  xpscf  17619  funcpropd  17959  isffth2  17975  eldmcoa  18122  setcinv  18147  xpccatid  18244  yonedainv  18337  ispos  18370  ispos2  18371  joinfval2  18428  meetfval2  18442  istsr2  18640  isnsg2  19222  isnsg4  19233  isgim  19332  oppgid  19426  oppgcntz  19434  symgfix2  19486  efgval2  19794  iscyg2  19952  dmdprdd  20071  subgdmdprd  20106  issrg  20270  oppr1  20432  opprunit  20459  opprirred  20504  isrnghm  20523  isrhm  20560  issubrng  20632  subsubrng2  20649  subsubrg2  20684  rngcinv  20722  ringcinv  20756  isdomn2  20796  islmim  21161  lbsextg  21264  lidlnz  21350  prmidl0  21447  resubdrg  21727  unocv  21799  pjfval2  21828  islinds2  21932  opsrtoslem1  22175  mdetunilem8  22745  istop2g  23022  isbasis2g  23074  tgval2  23082  isclo2  23214  isnrm2  23484  is1stc2  23568  llyi  23600  isfbas2  23961  elfg  23997  ufinffr  24055  isfcls  24135  alexsubALTlem2  24174  alexsubALTlem3  24175  cnextcn  24193  ustfilxp  24339  iscusp2  24427  metustid  24680  isclmp  25225  iscvsp  25256  tcphcph  25365  iscau3  25406  caucfil  25411  mdegleb  26190  plymulidp  26412  ellogdm  26770  dvdsflsumcom  27318  logfac2  27347  dchrelbas3  27368  dchrvmasumlema  27630  nosupno  27833  noinfno  27848  noinfbnd1lem1  27853  dmcuts  27950  made0  28022  mulsproplem5  28279  norecdiv  28349  elnnzs  28560  uzsind  28564  zsoring  28568  legtrid  28826  outpasch  28996  axcontlem5  29259  axcontlem6  29260  axcontlem7  29261  nb3grpr2  29674  iscplgr  29706  dfpth2  30019  pthdlem1  30056  wwlksnextinj  30189  usgr2wspthon  30258  rusgrnumwwlkl1  30261  isclwwlk  30276  clwwlkccatlem  30281  clwwlknon2x  30395  iseupthf1o  30494  frcond3  30561  frgr3v  30567  4cycl2vnunb  30582  frgrncvvdeqlem2  30592  fusgr2wsp2nb  30626  numclwlk1lem1  30661  hhcms  31496  isch3  31534  ocsh  31576  pjhtheu  31687  pjpreeq  31691  h1deoi  31842  h1dei  31843  eleigvec  32250  cvbr2  32576  cvnbtwn2  32580  cvnbtwn4  32582  mdsl2i  32615  cvmdi  32617  mdsymlem6  32701  cdj3lem3b  32733  mo5f  32776  nmo  32777  rexunirn  32779  dmrab  32784  difrab2  32785  disjunsn  32880  unipreima  32929  dfcnv2  32961  1stpreima  32993  isunit2  33500  lsmsnorb2  33649  ssmxidl  33702  1arithufdlem4  33782  ressply1mon1p  33803  extdgfialglem1  34027  zarcls  34209  rhmpreimacnlem  34219  isrnsiga  34448  rossros  34515  omsmeas  34658  eulerpartlemr  34709  eulerpartlemgvv  34711  ballotlemodife  34833  signstfvneq0  34904  bnj251  35036  bnj252  35037  bnj257  35041  bnj290  35044  bnj1304  35152  bnj153  35213  bnj543  35226  bnj571  35239  bnj580  35246  bnj607  35249  bnj882  35259  bnj964  35276  bnj996  35289  bnj1033  35302  bnj1176  35338  bnj1186  35340  bnj1189  35342  bnj1204  35345  bnj1253  35350  bnj1452  35385  bnj1463  35388  dff15  35416  axprALT2  35445  fineqvrep  35450  fineqvac  35452  lfuhgr3  35511  cusgredgex2  35514  usgrgt2cycl  35521  2cycl2d  35530  dfacycgr1  35535  erdszelem9  35590  cvmlift2lem9  35702  cvmlift2lem13  35706  satfvsucsuc  35756  satfdm  35760  satf0  35763  fmlasucdisj  35790  satffunlem  35792  satffunlem1lem1  35793  satffunlem2lem1  35795  elmthm  35967  axinfprim  36097  axacprim  36098  xpab  36117  dfso2  36146  dford5reg  36171  dfon2lem5  36176  dfon2  36181  brtxp2  36270  brpprod3a  36275  dfom5b  36301  brcart  36321  brimg  36326  funpartlem  36333  dfrecs2  36341  cgrxfr  36446  segletr  36505  sumeq2si  36603  prodeq2si  36605  cbvprodvw2  36648  trer  36716  fneval  36752  neifg  36771  df3nandALT1  36799  andnand1  36801  nandsym1  36822  weiunlem  36863  regsfromregtco  36938  mh-infprim2bi  36947  mh-infprim3bi  36948  bj-df-sb  37161  bj-dfsbc  37163  bj-eu3f  37365  bj-csbsnlem  37427  bj-snsetex  37487  bj-elsngl  37492  bj-snglc  37493  bj-restuni  37627  bj-dfmpoa  37648  bj-imdirco  37722  mptsnunlem  37872  icorempo  37885  isbasisrelowllem2  37890  relowlpssretop  37898  rdgeqoa  37904  difunieq  37908  dffinxpf  37919  nlpineqsn  37942  curf  38137  finixpnum  38144  ptrest  38158  poimirlem1  38160  poimirlem14  38173  poimirlem16  38175  poimirlem19  38178  poimirlem25  38184  poimirlem26  38185  poimirlem27  38186  poimir  38192  cnambfre  38207  itg2addnc  38213  ftc1anc  38240  opropabco  38263  isdrngo1  38495  keridl  38571  ispridlc  38609  selconj  38639  eldmres3  38822  eldmqsres  38832  cnvepres  38843  ecinn0  38892  alrmomorn  38897  moantr  38911  dfxrn2  38924  disjressuc2  38950  inxpxrn  38957  rnxrnres  38961  coss2cnvepres  39047  refrelredund4  39258  dferALTV2  39292  dfeldisj3  39350  dfpart2  39411  dfpeters2  39513  petseq  39515  prtlem70  39521  prtlem100  39523  prtlem15  39539  islshpat  39681  lcvbr2  39686  lcvbr3  39687  lcvnbtwn2  39691  ellkr  39753  cvrval2  39938  cvrnbtwn2  39939  cvrnbtwn3  39940  cvrnbtwn4  39943  ishlat2  40017  lplnexatN  40227  islvol5  40243  dath  40400  pclfinclN  40614  lhpexle3  40676  4atex2  40741  4atex2-0bOLDN  40743  isltrn2N  40784  cdleme0nex  40954  cdleme22b  41005  cdlemg17pq  41336  cdlemg19  41348  cdlemg21  41350  cdlemg33d  41373  dibopelvalN  41807  dibopelval2  41809  dib1dim  41829  dicelval2N  41846  diclspsn  41858  lcdlss  42283  mapd1o  42312  3factsumint2  42679  3factsumint3  42680  3factsumint  42682  hashnexinj  42785  sticksstones16  42819  sticksstones21  42824  unitscyglem3  42854  supinf  42900  fimgmcyclem  43193  eu6w  43300  mzpcompact2lem  43374  fz1eqin  43392  rexrabdioph  43413  expdiophlem1  43640  dford4  43648  fnwe2lem2  43670  fgraphopab  43822  dflim6  43883  onsucf1olem  43889  onsucrn  43890  nnoeomeqom  43931  faosnf0.11b  44045  ifpidg  44109  rp-fakeinunass  44133  rp-isfinite6  44136  dfsucon  44141  elinintrab  44195  elnonrel  44203  elmapintab  44214  dfrtrcl5  44247  imaiun1  44269  coiun1  44270  rfovcnvf1od  44622  andi3or  44642  uneqsn  44643  ntrneicls00  44707  rr-groth  44901  ismnushort  44903  rr-grothshortbi  44905  2sbc5g  45018  pm14.12  45023  2sb5nd  45161  uun2221  45413  uun2221p1  45414  uun2221p2  45415  2sb5ndVD  45510  2sb5ndALT  45532  modelaxreplem3  45581  iindif2f  45770  disjinfi  45802  climuz  46350  dfxlim2  46454  cncfshift  46480  dvnmul  46549  dvnprodlem2  46553  ismbl3  46592  ismbl4  46599  stoweidlem26  46632  stoweidlem35  46641  fourierdlem54  46766  fourierdlem83  46795  fourierdlem100  46812  fourierdlem104  46816  fourierdlem109  46821  fourierdlem112  46824  smfpimcc  47414  fcoresf1ob  47699  f1cof1b  47703  f1ocof1ob  47707  2reu8i  47739  dfdfat2  47754  ffnaov  47825  an4com24  47894  4an21  47896  iccpartiltu  48060  prproropf1olem0  48140  dfgric2  48569  gpgvtxedg0  48717  gpgvtxedg1  48718  gpgprismgr4cycllem10  48758  grlimedgnedg  48785  2zrngmmgm  48906  rngcinvALTV  48930  ringcinvALTV  48964  isprmrng  48990  pgrpgt2nabl  49031  islindeps  49118  lindslinindsimp1  49122  lindslinindsimp2  49128  ldepslinc  49174  blen1b  49253  coxp  49496  i0oii  49583  io1ii  49584  isthinc2  50083  isthinc3  50084  isthincd2  50100  istermc2  50138  istermc3  50139  dffun3f  50345  setrec1lem3  50352  elpglem3  50376  elpg  50377