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  1050  dn1  1058  dfifp3  1066  ifpdfbi  1071  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1526  cadcoma  1612  nic-mpALT  1672  nic-axALT  1674  3exdistr  1960  4exdistr  1961  19.27v  1989  19.27  2227  19.41  2235  2sb5  2278  dfsb7  2279  dfeumo  2537  mo4f  2567  eu3v  2570  eu6  2574  dfeu  2595  eu2  2609  eu4  2615  2mos  2649  2mosOLD  2650  2eu4  2655  r3ex  3198  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  reu2  3731  reu6  3732  reu4  3737  reu7  3738  rmo3f  3740  rmo4f  3741  2reu5lem3  3763  2reu5  3764  sbcimdv  3859  sbcg  3863  rmo3  3889  reuan  3896  dfpss2  4088  difdif  4135  raldifb  4149  inass  4228  dfss4  4269  dfin2  4271  indi  4284  indifdi  4294  undif3  4300  difin0ss  4373  inssdif0  4374  2nreu  4444  2reu4lem  4522  rexdifpr  4659  reuprg0  4702  ssdifsn  4788  ssunpr  4834  uniprg  4923  uniun  4930  uniin  4931  csbuni  4936  dfiun2g  5030  iunin2  5071  iundif2  5074  iindif2  5077  iinin2  5078  elpwpw  5102  axrep1  5280  axrep4v  5284  axrep4  5285  axrep4OLD  5286  reusv2lem4  5401  eqvinop  5492  opcom  5506  fconstmpt  5747  opeliunxp  5752  opeliun2xp  5753  xpundi  5754  elvvv  5761  opelinxp  5765  xpiindi  5846  elcnv2  5888  cnvuni  5897  dmuni  5925  brres  6004  dmres  6030  elidinxp  6062  restidsing  6071  elima3  6085  asymref  6136  imainss  6174  difxp  6184  xpdifid  6188  mptpreima  6258  coundir  6268  resco  6270  coass  6285  relrelss  6293  opreu2reurex  6314  dfpo2  6316  frpoind  6363  wfiOLD  6372  ordtri3or  6416  dffun2  6571  dffun2OLD  6572  dffun2OLDOLD  6573  dffun6  6574  dffun3  6575  dffun3OLD  6576  dffun4  6577  dffun5  6578  dffun6f  6579  dffun7  6593  dffun8  6594  dffun9  6595  svrelfun  6638  fncnv  6639  imadif  6650  dfmpt3  6702  fcnvres  6785  fint  6787  fin  6788  dff12  6803  fores  6830  dff1o4  6856  eqfnfv3  7053  fndmin  7065  fniniseg  7080  unpreima  7083  ffnfvf  7140  fsn2  7156  tpres  7221  fconstfv  7232  dff13f  7276  dff14a  7290  dff14b  7291  isocnv2  7351  f1opr  7489  eloprabga  7542  ffnov  7559  eqfnov  7562  foov  7607  uniuni  7782  tfindsg  7882  findsg  7919  funcnvuni  7954  opabex3d  7990  opabex3rd  7991  opabex3  7992  1stconst  8125  2ndconst  8126  frxp  8151  soxp  8154  xpord3lem  8174  suppvalbr  8189  suppofssd  8228  suppcoss  8232  mpoxopovel  8245  brtpos  8260  tpostpos  8271  dfsmo2  8387  dfrecs3  8412  dfrecs3OLD  8413  rdglem1  8455  tz7.49  8485  brwitnlem  8545  oeeu  8641  naddasslem2  8733  brinxper  8774  erinxp  8831  mapsncnv  8933  cbvixp  8954  cbvixpv  8955  ixpin  8963  ixpiin  8964  mptelixpg  8975  elixpsn  8977  ixpsnf1o  8978  xpassen  9106  omxpenlem  9113  sbthcl  9135  sbthfilem  9238  wemapsolem  9590  dford2  9660  inf2  9663  zfinf  9679  ttrclselem2  9766  trcl  9768  frind  9790  frr3g  9796  iscard2  10016  leweon  10051  aceq1  10157  dfac3  10161  dfac4  10162  dfac5lem2  10164  dfac5  10169  kmlem3  10193  kmlem4  10194  kmlem14  10204  kmlem15  10205  dfackm  10207  infmap2  10257  fin23lem25  10364  zorn2lem7  10542  brdom6disj  10572  zfcndrep  10654  zfcndinf  10658  fpwwe  10686  axgroth4  10872  grothprim  10874  grothtsk  10875  nqpr  11054  addsrmo  11113  mulsrmo  11114  opelreal  11170  elnnz  12623  elznn0nn  12627  peano2uz2  12706  nnwos  12957  dflt2  13190  xmullem  13306  4fvwrd4  13688  preduz  13690  elfznelfzo  13811  fzind2  13824  fsuppmapnn0fiubex  14033  hashinfxadd  14424  hashgt23el  14463  hashfun  14476  fi1uzind  14546  brfi1uzind  14547  opfi1uzind  14550  cotr2g  15015  shftdm  15110  rexfiuz  15386  cbvsum  15731  cbvsumv  15732  mertenslem2  15921  mertens  15922  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  prodmo  15972  iprodmul  16039  divalglem10  16439  ndvdssub  16446  bitsmod  16473  algcvgblem  16614  isprm2  16719  isprm4  16721  hashdvds  16812  infpn2  16951  hashbc0  17043  xpscf  17610  funcpropd  17947  isffth2  17963  eldmcoa  18110  setcinv  18135  xpccatid  18233  yonedainv  18326  ispos  18360  ispos2  18361  joinfval2  18419  meetfval2  18433  istsr2  18629  isnsg2  19174  isnsg4  19185  isgim  19280  oppgid  19375  oppgcntz  19383  symgfix2  19434  efgval2  19742  iscyg2  19900  dmdprdd  20019  subgdmdprd  20054  issrg  20185  oppr1  20350  opprunit  20377  opprirred  20422  isrnghm  20441  isrhm  20478  issubrng  20547  subsubrng2  20564  subsubrg2  20599  rngcinv  20637  ringcinv  20671  isdomn2  20711  isdomn2OLD  20712  islmim  21061  lbsextg  21164  lidlnz  21252  resubdrg  21626  unocv  21698  pjfval2  21729  islinds2  21833  opsrtoslem1  22079  mdetunilem8  22625  istop2g  22902  isbasis2g  22955  tgval2  22963  isclo2  23096  isnrm2  23366  is1stc2  23450  llyi  23482  isfbas2  23843  elfg  23879  ufinffr  23937  isfcls  24017  alexsubALTlem2  24056  alexsubALTlem3  24057  cnextcn  24075  ustfilxp  24221  iscusp2  24311  metustid  24567  isclmp  25130  iscvsp  25161  tcphcph  25271  iscau3  25312  caucfil  25317  mdegleb  26103  ellogdm  26681  dvdsflsumcom  27231  logfac2  27261  dchrelbas3  27282  dchrvmasumlema  27544  nosupno  27748  noinfno  27763  noinfbnd1lem1  27768  dmscut  27856  made0  27912  mulsproplem5  28146  norecdiv  28216  elnnzs  28387  uzsind  28391  legtrid  28599  outpasch  28763  axcontlem5  28983  axcontlem6  28984  axcontlem7  28985  nb3grpr2  29400  iscplgr  29432  dfpth2  29749  pthdlem1  29786  wwlksnextinj  29919  usgr2wspthon  29985  rusgrnumwwlkl1  29988  isclwwlk  30003  clwwlkccatlem  30008  clwwlknon2x  30122  iseupthf1o  30221  frcond3  30288  frgr3v  30294  4cycl2vnunb  30309  frgrncvvdeqlem2  30319  fusgr2wsp2nb  30353  numclwlk1lem1  30388  hhcms  31222  isch3  31260  ocsh  31302  pjhtheu  31413  pjpreeq  31417  h1deoi  31568  h1dei  31569  eleigvec  31976  cvbr2  32302  cvnbtwn2  32306  cvnbtwn4  32308  mdsl2i  32341  cvmdi  32343  mdsymlem6  32427  cdj3lem3b  32459  mo5f  32508  nmo  32509  rexunirn  32511  dmrab  32516  difrab2  32517  disjunsn  32607  unipreima  32653  dfcnv2  32686  1stpreima  32716  isunit2  33244  lsmsnorb2  33420  prmidl0  33478  ssmxidl  33502  1arithufdlem4  33575  ressply1mon1p  33593  zarcls  33873  rhmpreimacnlem  33883  isrnsiga  34114  rossros  34181  omsmeas  34325  eulerpartlemr  34376  eulerpartlemgvv  34378  ballotlemodife  34500  plymulx  34563  signstfvneq0  34587  bnj251  34716  bnj252  34717  bnj257  34721  bnj290  34724  bnj1304  34833  bnj153  34894  bnj543  34907  bnj571  34920  bnj580  34927  bnj607  34930  bnj882  34940  bnj964  34957  bnj996  34970  bnj1033  34983  bnj1176  35019  bnj1186  35021  bnj1189  35023  bnj1204  35026  bnj1253  35031  bnj1452  35066  bnj1463  35069  dff15  35098  fineqvrep  35109  fineqvac  35111  lfuhgr3  35125  cusgredgex2  35128  usgrgt2cycl  35135  2cycl2d  35144  dfacycgr1  35149  erdszelem9  35204  cvmlift2lem9  35316  cvmlift2lem13  35320  satfvsucsuc  35370  satfdm  35374  satf0  35377  fmlasucdisj  35404  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  elmthm  35581  axinfprim  35706  axacprim  35707  xpab  35726  dfso2  35755  dford5reg  35783  dfon2lem5  35788  dfon2  35793  brtxp2  35882  brpprod3a  35887  dfom5b  35913  brcart  35933  brimg  35938  funpartlem  35943  dfrecs2  35951  cgrxfr  36056  segletr  36115  sumeq2si  36203  prodeq2si  36205  cbvprodvw2  36248  trer  36317  fneval  36353  neifg  36372  df3nandALT1  36400  andnand1  36402  nandsym1  36423  weiunlem2  36464  bj-eu3f  36842  bj-csbsnlem  36904  bj-snsetex  36964  bj-elsngl  36969  bj-snglc  36970  bj-restuni  37098  bj-dfmpoa  37119  bj-imdirco  37191  mptsnunlem  37339  icorempo  37352  isbasisrelowllem2  37357  relowlpssretop  37365  rdgeqoa  37371  difunieq  37375  dffinxpf  37386  nlpineqsn  37409  curf  37605  finixpnum  37612  ptrest  37626  poimirlem1  37628  poimirlem14  37641  poimirlem16  37643  poimirlem19  37646  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimir  37660  cnambfre  37675  itg2addnc  37681  ftc1anc  37708  opropabco  37731  isdrngo1  37963  keridl  38039  ispridlc  38077  selconj  38107  eldmqsres  38288  cnvepres  38299  ecinn0  38354  alrmomorn  38359  moantr  38365  dfxrn2  38377  disjressuc2  38389  inxpxrn  38396  rnxrnres  38400  coss2cnvepres  38419  refrelredund4  38636  dferALTV2  38669  dfeldisj3  38720  dfpart2  38770  prtlem70  38858  prtlem100  38860  prtlem15  38876  islshpat  39018  lcvbr2  39023  lcvbr3  39024  lcvnbtwn2  39028  ellkr  39090  cvrval2  39275  cvrnbtwn2  39276  cvrnbtwn3  39277  cvrnbtwn4  39280  ishlat2  39354  lplnexatN  39565  islvol5  39581  dath  39738  pclfinclN  39952  lhpexle3  40014  4atex2  40079  4atex2-0bOLDN  40081  isltrn2N  40122  cdleme0nex  40292  cdleme22b  40343  cdlemg17pq  40674  cdlemg19  40686  cdlemg21  40688  cdlemg33d  40711  dibopelvalN  41145  dibopelval2  41147  dib1dim  41167  dicelval2N  41184  diclspsn  41196  lcdlss  41621  mapd1o  41650  3factsumint2  42023  3factsumint3  42024  3factsumint  42026  hashnexinj  42129  sticksstones16  42163  sticksstones21  42168  unitscyglem3  42198  metakunt1  42206  supinf  42283  fimgmcyclem  42543  eu6w  42686  mzpcompact2lem  42762  fz1eqin  42780  rexrabdioph  42805  expdiophlem1  43033  dford4  43041  fnwe2lem2  43063  fgraphopab  43215  dflim6  43277  onsucf1olem  43283  onsucrn  43284  nnoeomeqom  43325  faosnf0.11b  43440  ifpidg  43504  rp-fakeinunass  43528  rp-isfinite6  43531  dfsucon  43536  elinintrab  43590  elnonrel  43598  elmapintab  43609  dfrtrcl5  43642  imaiun1  43664  coiun1  43665  rfovcnvf1od  44017  andi3or  44037  uneqsn  44038  ntrneicls00  44102  rr-groth  44318  ismnushort  44320  rr-grothshortbi  44322  2sbc5g  44435  pm14.12  44440  2sb5nd  44580  uun2221  44833  uun2221p1  44834  uun2221p2  44835  2sb5ndVD  44930  2sb5ndALT  44952  modelaxreplem3  44997  iindif2f  45165  disjinfi  45197  climuz  45759  dfxlim2  45863  cncfshift  45889  dvnmul  45958  dvnprodlem2  45962  ismbl3  46001  ismbl4  46008  stoweidlem26  46041  stoweidlem35  46050  fourierdlem54  46175  fourierdlem83  46204  fourierdlem100  46221  fourierdlem104  46225  fourierdlem109  46230  fourierdlem112  46233  smfpimcc  46823  fcoresf1ob  47085  f1cof1b  47089  f1ocof1ob  47093  2reu8i  47125  dfdfat2  47140  ffnaov  47211  an4com24  47280  4an21  47282  iccpartiltu  47409  prproropf1olem0  47489  dfgric2  47884  gpgvtxedg0  48021  gpgvtxedg1  48022  2zrngmmgm  48168  rngcinvALTV  48192  ringcinvALTV  48226  pgrpgt2nabl  48282  islindeps  48370  lindslinindsimp1  48374  lindslinindsimp2  48380  ldepslinc  48426  blen1b  48509  coxp  48744  i0oii  48817  io1ii  48818  isthinc2  49070  isthinc3  49071  isthincd2  49086  istermc2  49122  istermc3  49123  dffun3f  49201  setrec1lem3  49208  elpglem3  49232  elpg  49233