Theorem anbi2i 623

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  626  anbi12i  628  bianass  642  an42  657  anandir  677  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1527  cadcoma  1613  nic-mpALT  1673  nic-axALT  1675  3exdistr  1961  4exdistr  1962  19.27v  1996  19.27  2232  19.41  2240  2sb5  2282  dfsb7  2283  dfeumo  2534  mo4f  2565  eu3v  2568  eu6  2572  dfeu  2593  eu2  2607  eu4  2613  2mos  2647  2mosOLD  2648  2eu4  2653  r3ex  3173  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  reu2  3681  reu6  3682  reu4  3687  reu7  3688  rmo3f  3690  rmo4f  3691  2reu5lem3  3713  2reu5  3714  sbcimdv  3807  sbcg  3811  rmo3  3837  reuan  3844  dfpss2  4038  difdif  4085  raldifb  4099  inass  4178  dfss4  4219  dfin2  4221  indi  4234  indifdi  4244  undif3  4250  difin0ss  4323  inssdif0  4324  2nreu  4394  2reu4lem  4474  rexdifpr  4614  reuprg0  4657  ssdifsn  4742  ssunpr  4788  uniprg  4877  uniun  4884  uniin  4885  csbuni  4891  dfiun2g  4983  iunin2  5024  iundif2  5027  iindif2  5030  iinin2  5031  elpwpw  5055  axrep1  5223  axrep4v  5227  axrep4  5228  axrep4OLD  5229  reusv2lem4  5344  eqvinop  5433  opcom  5447  fconstmpt  5684  opeliunxp  5689  opeliun2xp  5690  xpundi  5691  elvvv  5698  opelinxp  5702  xpiindi  5782  elcnv2  5824  cnvuni  5833  dmuni  5861  brres  5943  dmres  5969  elidinxp  6001  restidsing  6010  elima3  6024  asymref  6071  imainss  6110  difxp  6120  xpdifid  6124  mptpreima  6194  coundir  6204  resco  6206  coass  6222  relrelss  6229  opreu2reurex  6250  dfpo2  6252  frpoind  6298  ordtri3or  6347  dffun2  6500  dffun6  6501  dffun3  6502  dffun4  6503  dffun5  6504  dffun6f  6505  dffun7  6517  dffun8  6518  dffun9  6519  svrelfun  6562  fncnv  6563  imadif  6574  dfmpt3  6624  fcnvres  6709  fint  6711  fin  6712  dff12  6727  fores  6754  dff1o4  6780  eqfnfv3  6976  fndmin  6988  fniniseg  7003  unpreima  7006  ffnfvf  7063  fsn2  7079  tpres  7145  fconstfv  7156  dff13f  7199  dff14a  7214  dff14b  7215  isocnv2  7275  f1opr  7412  eloprabga  7465  ffnov  7482  eqfnov  7485  foov  7530  uniuni  7705  tfindsg  7801  findsg  7837  funcnvuni  7872  opabex3d  7907  opabex3rd  7908  opabex3  7909  1stconst  8040  2ndconst  8041  frxp  8066  soxp  8069  xpord3lem  8089  suppvalbr  8104  suppofssd  8143  suppcoss  8147  mpoxopovel  8160  brtpos  8175  tpostpos  8186  dfsmo2  8277  dfrecs3  8302  rdglem1  8344  tz7.49  8374  brwitnlem  8432  oeeu  8529  naddasslem2  8621  brinxper  8662  erinxp  8726  mapsncnv  8829  cbvixp  8850  cbvixpv  8851  ixpin  8859  ixpiin  8860  mptelixpg  8871  elixpsn  8873  ixpsnf1o  8874  xpassen  8997  omxpenlem  9004  sbthcl  9025  sbthfilem  9120  wemapsolem  9453  dford2  9527  inf2  9530  zfinf  9546  ttrclselem2  9633  trcl  9635  frind  9660  frr3g  9666  iscard2  9886  leweon  9919  aceq1  10025  dfac3  10029  dfac4  10030  dfac5lem2  10032  dfac5  10037  kmlem3  10061  kmlem4  10062  kmlem14  10072  kmlem15  10073  dfackm  10075  infmap2  10125  fin23lem25  10232  zorn2lem7  10410  brdom6disj  10440  zfcndrep  10523  zfcndinf  10527  fpwwe  10555  axgroth4  10741  grothprim  10743  grothtsk  10744  nqpr  10923  addsrmo  10982  mulsrmo  10983  opelreal  11039  elnnz  12496  elznn0nn  12500  peano2uz2  12578  nnwos  12826  dflt2  13060  xmullem  13177  4fvwrd4  13562  preduz  13564  elfznelfzo  13687  fzind2  13702  fsuppmapnn0fiubex  13913  hashinfxadd  14306  hashgt23el  14345  hashfun  14358  fi1uzind  14428  brfi1uzind  14429  opfi1uzind  14432  cotr2g  14897  shftdm  14992  rexfiuz  15269  cbvsum  15616  cbvsumv  15617  mertenslem2  15806  mertens  15807  cbvprod  15834  cbvprodv  15835  prodeq1i  15837  prodmo  15857  iprodmul  15924  divalglem10  16327  ndvdssub  16334  bitsmod  16361  algcvgblem  16502  isprm2  16607  isprm4  16609  hashdvds  16700  infpn2  16839  hashbc0  16931  xpscf  17484  funcpropd  17824  isffth2  17840  eldmcoa  17987  setcinv  18012  xpccatid  18109  yonedainv  18202  ispos  18235  ispos2  18236  joinfval2  18293  meetfval2  18307  istsr2  18505  isnsg2  19083  isnsg4  19094  isgim  19189  oppgid  19283  oppgcntz  19291  symgfix2  19343  efgval2  19651  iscyg2  19809  dmdprdd  19928  subgdmdprd  19963  issrg  20121  oppr1  20284  opprunit  20311  opprirred  20356  isrnghm  20375  isrhm  20412  issubrng  20478  subsubrng2  20495  subsubrg2  20530  rngcinv  20568  ringcinv  20602  isdomn2  20642  isdomn2OLD  20643  islmim  21012  lbsextg  21115  lidlnz  21195  resubdrg  21561  unocv  21633  pjfval2  21662  islinds2  21766  opsrtoslem1  22008  mdetunilem8  22561  istop2g  22838  isbasis2g  22890  tgval2  22898  isclo2  23030  isnrm2  23300  is1stc2  23384  llyi  23416  isfbas2  23777  elfg  23813  ufinffr  23871  isfcls  23951  alexsubALTlem2  23990  alexsubALTlem3  23991  cnextcn  24009  ustfilxp  24155  iscusp2  24243  metustid  24496  isclmp  25051  iscvsp  25082  tcphcph  25191  iscau3  25232  caucfil  25237  mdegleb  26023  ellogdm  26602  dvdsflsumcom  27152  logfac2  27182  dchrelbas3  27203  dchrvmasumlema  27465  nosupno  27669  noinfno  27684  noinfbnd1lem1  27689  dmscut  27779  made0  27845  mulsproplem5  28089  norecdiv  28159  elnnzs  28359  uzsind  28363  zsoring  28367  legtrid  28612  outpasch  28776  axcontlem5  28990  axcontlem6  28991  axcontlem7  28992  nb3grpr2  29405  iscplgr  29437  dfpth2  29751  pthdlem1  29788  wwlksnextinj  29921  usgr2wspthon  29990  rusgrnumwwlkl1  29993  isclwwlk  30008  clwwlkccatlem  30013  clwwlknon2x  30127  iseupthf1o  30226  frcond3  30293  frgr3v  30299  4cycl2vnunb  30314  frgrncvvdeqlem2  30324  fusgr2wsp2nb  30358  numclwlk1lem1  30393  hhcms  31227  isch3  31265  ocsh  31307  pjhtheu  31418  pjpreeq  31422  h1deoi  31573  h1dei  31574  eleigvec  31981  cvbr2  32307  cvnbtwn2  32311  cvnbtwn4  32313  mdsl2i  32346  cvmdi  32348  mdsymlem6  32432  cdj3lem3b  32464  mo5f  32512  nmo  32513  rexunirn  32515  dmrab  32520  difrab2  32521  disjunsn  32618  unipreima  32670  dfcnv2  32703  1stpreima  32735  isunit2  33271  lsmsnorb2  33422  prmidl0  33480  ssmxidl  33504  1arithufdlem4  33577  ressply1mon1p  33598  extdgfialglem1  33798  zarcls  33980  rhmpreimacnlem  33990  isrnsiga  34219  rossros  34286  omsmeas  34429  eulerpartlemr  34480  eulerpartlemgvv  34482  ballotlemodife  34604  plymulx  34654  signstfvneq0  34678  bnj251  34807  bnj252  34808  bnj257  34812  bnj290  34815  bnj1304  34924  bnj153  34985  bnj543  34998  bnj571  35011  bnj580  35018  bnj607  35021  bnj882  35031  bnj964  35048  bnj996  35061  bnj1033  35074  bnj1176  35110  bnj1186  35112  bnj1189  35114  bnj1204  35117  bnj1253  35122  bnj1452  35157  bnj1463  35160  dff15  35189  fineqvrep  35219  fineqvac  35221  lfuhgr3  35263  cusgredgex2  35266  usgrgt2cycl  35273  2cycl2d  35282  dfacycgr1  35287  erdszelem9  35342  cvmlift2lem9  35454  cvmlift2lem13  35458  satfvsucsuc  35508  satfdm  35512  satf0  35515  fmlasucdisj  35542  satffunlem  35544  satffunlem1lem1  35545  satffunlem2lem1  35547  elmthm  35719  axinfprim  35849  axacprim  35850  xpab  35869  dfso2  35898  dford5reg  35923  dfon2lem5  35928  dfon2  35933  brtxp2  36022  brpprod3a  36027  dfom5b  36053  brcart  36073  brimg  36078  funpartlem  36085  dfrecs2  36093  cgrxfr  36198  segletr  36257  sumeq2si  36345  prodeq2si  36347  cbvprodvw2  36390  trer  36459  fneval  36495  neifg  36514  df3nandALT1  36542  andnand1  36544  nandsym1  36565  weiunlem2  36606  bj-df-sb  36796  bj-eu3f  36985  bj-csbsnlem  37047  bj-snsetex  37107  bj-elsngl  37112  bj-snglc  37113  bj-restuni  37241  bj-dfmpoa  37262  bj-imdirco  37334  mptsnunlem  37482  icorempo  37495  isbasisrelowllem2  37500  relowlpssretop  37508  rdgeqoa  37514  difunieq  37518  dffinxpf  37529  nlpineqsn  37552  curf  37738  finixpnum  37745  ptrest  37759  poimirlem1  37761  poimirlem14  37774  poimirlem16  37776  poimirlem19  37779  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  poimir  37793  cnambfre  37808  itg2addnc  37814  ftc1anc  37841  opropabco  37864  isdrngo1  38096  keridl  38172  ispridlc  38210  selconj  38240  eldmres3  38415  eldmqsres  38425  cnvepres  38436  ecinn0  38485  alrmomorn  38490  moantr  38496  dfxrn2  38509  disjressuc2  38535  inxpxrn  38542  rnxrnres  38546  coss2cnvepres  38620  refrelredund4  38831  dfblockliftfix2  38836  dferALTV2  38866  dfeldisj3  38917  dfpart2  38967  prtlem70  39056  prtlem100  39058  prtlem15  39074  islshpat  39216  lcvbr2  39221  lcvbr3  39222  lcvnbtwn2  39226  ellkr  39288  cvrval2  39473  cvrnbtwn2  39474  cvrnbtwn3  39475  cvrnbtwn4  39478  ishlat2  39552  lplnexatN  39762  islvol5  39778  dath  39935  pclfinclN  40149  lhpexle3  40211  4atex2  40276  4atex2-0bOLDN  40278  isltrn2N  40319  cdleme0nex  40489  cdleme22b  40540  cdlemg17pq  40871  cdlemg19  40883  cdlemg21  40885  cdlemg33d  40908  dibopelvalN  41342  dibopelval2  41344  dib1dim  41364  dicelval2N  41381  diclspsn  41393  lcdlss  41818  mapd1o  41847  3factsumint2  42215  3factsumint3  42216  3factsumint  42218  hashnexinj  42321  sticksstones16  42355  sticksstones21  42360  unitscyglem3  42390  supinf  42439  fimgmcyclem  42730  eu6w  42861  mzpcompact2lem  42935  fz1eqin  42953  rexrabdioph  42978  expdiophlem1  43205  dford4  43213  fnwe2lem2  43235  fgraphopab  43387  dflim6  43448  onsucf1olem  43454  onsucrn  43455  nnoeomeqom  43496  faosnf0.11b  43610  ifpidg  43674  rp-fakeinunass  43698  rp-isfinite6  43701  dfsucon  43706  elinintrab  43760  elnonrel  43768  elmapintab  43779  dfrtrcl5  43812  imaiun1  43834  coiun1  43835  rfovcnvf1od  44187  andi3or  44207  uneqsn  44208  ntrneicls00  44272  rr-groth  44482  ismnushort  44484  rr-grothshortbi  44486  2sbc5g  44599  pm14.12  44604  2sb5nd  44743  uun2221  44995  uun2221p1  44996  uun2221p2  44997  2sb5ndVD  45092  2sb5ndALT  45114  modelaxreplem3  45163  iindif2f  45346  disjinfi  45378  climuz  45930  dfxlim2  46034  cncfshift  46060  dvnmul  46129  dvnprodlem2  46133  ismbl3  46172  ismbl4  46179  stoweidlem26  46212  stoweidlem35  46221  fourierdlem54  46346  fourierdlem83  46375  fourierdlem100  46392  fourierdlem104  46396  fourierdlem109  46401  fourierdlem112  46404  smfpimcc  46994  fcoresf1ob  47261  f1cof1b  47265  f1ocof1ob  47269  2reu8i  47301  dfdfat2  47316  ffnaov  47387  an4com24  47456  4an21  47458  iccpartiltu  47610  prproropf1olem0  47690  dfgric2  48103  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgprismgr4cycllem10  48292  grlimedgnedg  48319  2zrngmmgm  48440  rngcinvALTV  48464  ringcinvALTV  48498  pgrpgt2nabl  48554  islindeps  48641  lindslinindsimp1  48645  lindslinindsimp2  48651  ldepslinc  48697  blen1b  48776  coxp  49020  i0oii  49107  io1ii  49108  isthinc2  49607  isthinc3  49608  isthincd2  49624  istermc2  49662  istermc3  49663  dffun3f  49869  setrec1lem3  49876  elpglem3  49900  elpg  49901