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  2230  19.41  2238  2sb5  2280  dfsb7  2281  dfeumo  2532  mo4f  2562  eu3v  2565  eu6  2569  dfeu  2590  eu2  2604  eu4  2610  2mos  2644  2mosOLD  2645  2eu4  2650  r3ex  3171  ceqsex3v  3491  ceqsex4v  3492  ceqsex8v  3494  reu2  3679  reu6  3680  reu4  3685  reu7  3686  rmo3f  3688  rmo4f  3689  2reu5lem3  3711  2reu5  3712  sbcimdv  3805  sbcg  3809  rmo3  3835  reuan  3842  dfpss2  4035  difdif  4082  raldifb  4096  inass  4175  dfss4  4216  dfin2  4218  indi  4231  indifdi  4241  undif3  4247  difin0ss  4320  inssdif0  4321  2nreu  4391  2reu4lem  4469  rexdifpr  4609  reuprg0  4652  ssdifsn  4737  ssunpr  4783  uniprg  4872  uniun  4879  uniin  4880  csbuni  4886  dfiun2g  4978  iunin2  5017  iundif2  5020  iindif2  5023  iinin2  5024  elpwpw  5048  axrep1  5216  axrep4v  5220  axrep4  5221  axrep4OLD  5222  reusv2lem4  5337  eqvinop  5425  opcom  5439  fconstmpt  5676  opeliunxp  5681  opeliun2xp  5682  xpundi  5683  elvvv  5690  opelinxp  5694  xpiindi  5774  elcnv2  5816  cnvuni  5825  dmuni  5853  brres  5934  dmres  5960  elidinxp  5992  restidsing  6001  elima3  6015  asymref  6062  imainss  6101  difxp  6111  xpdifid  6115  mptpreima  6185  coundir  6195  resco  6197  coass  6213  relrelss  6220  opreu2reurex  6241  dfpo2  6243  frpoind  6289  ordtri3or  6338  dffun2  6491  dffun6  6492  dffun3  6493  dffun4  6494  dffun5  6495  dffun6f  6496  dffun7  6508  dffun8  6509  dffun9  6510  svrelfun  6553  fncnv  6554  imadif  6565  dfmpt3  6615  fcnvres  6700  fint  6702  fin  6703  dff12  6718  fores  6745  dff1o4  6771  eqfnfv3  6966  fndmin  6978  fniniseg  6993  unpreima  6996  ffnfvf  7053  fsn2  7069  tpres  7135  fconstfv  7146  dff13f  7189  dff14a  7204  dff14b  7205  isocnv2  7265  f1opr  7402  eloprabga  7455  ffnov  7472  eqfnov  7475  foov  7520  uniuni  7695  tfindsg  7791  findsg  7827  funcnvuni  7862  opabex3d  7897  opabex3rd  7898  opabex3  7899  1stconst  8030  2ndconst  8031  frxp  8056  soxp  8059  xpord3lem  8079  suppvalbr  8094  suppofssd  8133  suppcoss  8137  mpoxopovel  8150  brtpos  8165  tpostpos  8176  dfsmo2  8267  dfrecs3  8292  rdglem1  8334  tz7.49  8364  brwitnlem  8422  oeeu  8518  naddasslem2  8610  brinxper  8651  erinxp  8715  mapsncnv  8817  cbvixp  8838  cbvixpv  8839  ixpin  8847  ixpiin  8848  mptelixpg  8859  elixpsn  8861  ixpsnf1o  8862  xpassen  8984  omxpenlem  8991  sbthcl  9012  sbthfilem  9107  wemapsolem  9436  dford2  9510  inf2  9513  zfinf  9529  ttrclselem2  9616  trcl  9618  frind  9643  frr3g  9649  iscard2  9869  leweon  9902  aceq1  10008  dfac3  10012  dfac4  10013  dfac5lem2  10015  dfac5  10020  kmlem3  10044  kmlem4  10045  kmlem14  10055  kmlem15  10056  dfackm  10058  infmap2  10108  fin23lem25  10215  zorn2lem7  10393  brdom6disj  10423  zfcndrep  10505  zfcndinf  10509  fpwwe  10537  axgroth4  10723  grothprim  10725  grothtsk  10726  nqpr  10905  addsrmo  10964  mulsrmo  10965  opelreal  11021  elnnz  12478  elznn0nn  12482  peano2uz2  12561  nnwos  12813  dflt2  13047  xmullem  13163  4fvwrd4  13548  preduz  13550  elfznelfzo  13673  fzind2  13688  fsuppmapnn0fiubex  13899  hashinfxadd  14292  hashgt23el  14331  hashfun  14344  fi1uzind  14414  brfi1uzind  14415  opfi1uzind  14418  cotr2g  14883  shftdm  14978  rexfiuz  15255  cbvsum  15602  cbvsumv  15603  mertenslem2  15792  mertens  15793  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  prodmo  15843  iprodmul  15910  divalglem10  16313  ndvdssub  16320  bitsmod  16347  algcvgblem  16488  isprm2  16593  isprm4  16595  hashdvds  16686  infpn2  16825  hashbc0  16917  xpscf  17469  funcpropd  17809  isffth2  17825  eldmcoa  17972  setcinv  17997  xpccatid  18094  yonedainv  18187  ispos  18220  ispos2  18221  joinfval2  18278  meetfval2  18292  istsr2  18490  isnsg2  19068  isnsg4  19079  isgim  19174  oppgid  19268  oppgcntz  19276  symgfix2  19328  efgval2  19636  iscyg2  19794  dmdprdd  19913  subgdmdprd  19948  issrg  20106  oppr1  20268  opprunit  20295  opprirred  20340  isrnghm  20359  isrhm  20396  issubrng  20462  subsubrng2  20479  subsubrg2  20514  rngcinv  20552  ringcinv  20586  isdomn2  20626  isdomn2OLD  20627  islmim  20996  lbsextg  21099  lidlnz  21179  resubdrg  21545  unocv  21617  pjfval2  21646  islinds2  21750  opsrtoslem1  21990  mdetunilem8  22534  istop2g  22811  isbasis2g  22863  tgval2  22871  isclo2  23003  isnrm2  23273  is1stc2  23357  llyi  23389  isfbas2  23750  elfg  23786  ufinffr  23844  isfcls  23924  alexsubALTlem2  23963  alexsubALTlem3  23964  cnextcn  23982  ustfilxp  24128  iscusp2  24216  metustid  24469  isclmp  25024  iscvsp  25055  tcphcph  25164  iscau3  25205  caucfil  25210  mdegleb  25996  ellogdm  26575  dvdsflsumcom  27125  logfac2  27155  dchrelbas3  27176  dchrvmasumlema  27438  nosupno  27642  noinfno  27657  noinfbnd1lem1  27662  dmscut  27752  made0  27818  mulsproplem5  28059  norecdiv  28129  elnnzs  28325  uzsind  28329  zsoring  28332  legtrid  28569  outpasch  28733  axcontlem5  28946  axcontlem6  28947  axcontlem7  28948  nb3grpr2  29361  iscplgr  29393  dfpth2  29707  pthdlem1  29744  wwlksnextinj  29877  usgr2wspthon  29946  rusgrnumwwlkl1  29949  isclwwlk  29964  clwwlkccatlem  29969  clwwlknon2x  30083  iseupthf1o  30182  frcond3  30249  frgr3v  30255  4cycl2vnunb  30270  frgrncvvdeqlem2  30280  fusgr2wsp2nb  30314  numclwlk1lem1  30349  hhcms  31183  isch3  31221  ocsh  31263  pjhtheu  31374  pjpreeq  31378  h1deoi  31529  h1dei  31530  eleigvec  31937  cvbr2  32263  cvnbtwn2  32267  cvnbtwn4  32269  mdsl2i  32302  cvmdi  32304  mdsymlem6  32388  cdj3lem3b  32420  mo5f  32468  nmo  32469  rexunirn  32471  dmrab  32476  difrab2  32477  disjunsn  32574  unipreima  32625  dfcnv2  32658  1stpreima  32688  isunit2  33207  lsmsnorb2  33357  prmidl0  33415  ssmxidl  33439  1arithufdlem4  33512  ressply1mon1p  33531  extdgfialglem1  33705  zarcls  33887  rhmpreimacnlem  33897  isrnsiga  34126  rossros  34193  omsmeas  34336  eulerpartlemr  34387  eulerpartlemgvv  34389  ballotlemodife  34511  plymulx  34561  signstfvneq0  34585  bnj251  34714  bnj252  34715  bnj257  34719  bnj290  34722  bnj1304  34831  bnj153  34892  bnj543  34905  bnj571  34918  bnj580  34925  bnj607  34928  bnj882  34938  bnj964  34955  bnj996  34968  bnj1033  34981  bnj1176  35017  bnj1186  35019  bnj1189  35021  bnj1204  35024  bnj1253  35029  bnj1452  35064  bnj1463  35067  dff15  35096  fineqvrep  35137  fineqvac  35139  lfuhgr3  35164  cusgredgex2  35167  usgrgt2cycl  35174  2cycl2d  35183  dfacycgr1  35188  erdszelem9  35243  cvmlift2lem9  35355  cvmlift2lem13  35359  satfvsucsuc  35409  satfdm  35413  satf0  35416  fmlasucdisj  35443  satffunlem  35445  satffunlem1lem1  35446  satffunlem2lem1  35448  elmthm  35620  axinfprim  35750  axacprim  35751  xpab  35770  dfso2  35799  dford5reg  35824  dfon2lem5  35829  dfon2  35834  brtxp2  35923  brpprod3a  35928  dfom5b  35954  brcart  35974  brimg  35979  funpartlem  35984  dfrecs2  35992  cgrxfr  36097  segletr  36156  sumeq2si  36244  prodeq2si  36246  cbvprodvw2  36289  trer  36358  fneval  36394  neifg  36413  df3nandALT1  36441  andnand1  36443  nandsym1  36464  weiunlem2  36505  bj-eu3f  36883  bj-csbsnlem  36945  bj-snsetex  37005  bj-elsngl  37010  bj-snglc  37011  bj-restuni  37139  bj-dfmpoa  37160  bj-imdirco  37232  mptsnunlem  37380  icorempo  37393  isbasisrelowllem2  37398  relowlpssretop  37406  rdgeqoa  37412  difunieq  37416  dffinxpf  37427  nlpineqsn  37450  curf  37646  finixpnum  37653  ptrest  37667  poimirlem1  37669  poimirlem14  37682  poimirlem16  37684  poimirlem19  37687  poimirlem25  37693  poimirlem26  37694  poimirlem27  37695  poimir  37701  cnambfre  37716  itg2addnc  37722  ftc1anc  37749  opropabco  37772  isdrngo1  38004  keridl  38080  ispridlc  38118  selconj  38148  eldmres3  38319  eldmqsres  38329  cnvepres  38340  ecinn0  38389  alrmomorn  38394  moantr  38400  dfxrn2  38412  disjressuc2  38428  inxpxrn  38435  rnxrnres  38439  coss2cnvepres  38463  refrelredund4  38680  dferALTV2  38714  dfeldisj3  38765  dfpart2  38815  prtlem70  38904  prtlem100  38906  prtlem15  38922  islshpat  39064  lcvbr2  39069  lcvbr3  39070  lcvnbtwn2  39074  ellkr  39136  cvrval2  39321  cvrnbtwn2  39322  cvrnbtwn3  39323  cvrnbtwn4  39326  ishlat2  39400  lplnexatN  39610  islvol5  39626  dath  39783  pclfinclN  39997  lhpexle3  40059  4atex2  40124  4atex2-0bOLDN  40126  isltrn2N  40167  cdleme0nex  40337  cdleme22b  40388  cdlemg17pq  40719  cdlemg19  40731  cdlemg21  40733  cdlemg33d  40756  dibopelvalN  41190  dibopelval2  41192  dib1dim  41212  dicelval2N  41229  diclspsn  41241  lcdlss  41666  mapd1o  41695  3factsumint2  42063  3factsumint3  42064  3factsumint  42066  hashnexinj  42169  sticksstones16  42203  sticksstones21  42208  unitscyglem3  42238  supinf  42283  fimgmcyclem  42574  eu6w  42717  mzpcompact2lem  42792  fz1eqin  42810  rexrabdioph  42835  expdiophlem1  43062  dford4  43070  fnwe2lem2  43092  fgraphopab  43244  dflim6  43305  onsucf1olem  43311  onsucrn  43312  nnoeomeqom  43353  faosnf0.11b  43468  ifpidg  43532  rp-fakeinunass  43556  rp-isfinite6  43559  dfsucon  43564  elinintrab  43618  elnonrel  43626  elmapintab  43637  dfrtrcl5  43670  imaiun1  43692  coiun1  43693  rfovcnvf1od  44045  andi3or  44065  uneqsn  44066  ntrneicls00  44130  rr-groth  44340  ismnushort  44342  rr-grothshortbi  44344  2sbc5g  44457  pm14.12  44462  2sb5nd  44601  uun2221  44853  uun2221p1  44854  uun2221p2  44855  2sb5ndVD  44950  2sb5ndALT  44972  modelaxreplem3  45021  iindif2f  45205  disjinfi  45237  climuz  45790  dfxlim2  45894  cncfshift  45920  dvnmul  45989  dvnprodlem2  45993  ismbl3  46032  ismbl4  46039  stoweidlem26  46072  stoweidlem35  46081  fourierdlem54  46206  fourierdlem83  46235  fourierdlem100  46252  fourierdlem104  46256  fourierdlem109  46261  fourierdlem112  46264  smfpimcc  46854  fcoresf1ob  47112  f1cof1b  47116  f1ocof1ob  47120  2reu8i  47152  dfdfat2  47167  ffnaov  47238  an4com24  47307  4an21  47309  iccpartiltu  47461  prproropf1olem0  47541  dfgric2  47954  gpgvtxedg0  48102  gpgvtxedg1  48103  gpgprismgr4cycllem10  48143  grlimedgnedg  48170  2zrngmmgm  48291  rngcinvALTV  48315  ringcinvALTV  48349  pgrpgt2nabl  48405  islindeps  48493  lindslinindsimp1  48497  lindslinindsimp2  48503  ldepslinc  48549  blen1b  48628  coxp  48872  i0oii  48959  io1ii  48960  isthinc2  49460  isthinc3  49461  isthincd2  49477  istermc2  49515  istermc3  49516  dffun3f  49722  setrec1lem3  49729  elpglem3  49753  elpg  49754