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  3177  ceqsex3v  3497  ceqsex4v  3498  ceqsex8v  3500  reu2  3685  reu6  3686  reu4  3691  reu7  3692  rmo3f  3694  rmo4f  3695  2reu5lem3  3717  2reu5  3718  sbcimdv  3811  sbcg  3815  rmo3  3841  reuan  3848  dfpss2  4042  difdif  4089  raldifb  4103  inass  4182  dfss4  4223  dfin2  4225  indi  4238  indifdi  4248  undif3  4254  difin0ss  4327  inssdif0  4328  2nreu  4398  2reu4lem  4478  rexdifpr  4618  reuprg0  4661  ssdifsn  4746  ssunpr  4792  uniprg  4881  uniun  4888  uniin  4889  csbuni  4895  dfiun2g  4987  iunin2  5028  iundif2  5031  iindif2  5034  iinin2  5035  elpwpw  5059  axrep1  5227  axrep4v  5231  axrep4  5232  axrep4OLD  5233  reusv2lem4  5348  eqvinop  5443  opcom  5457  fconstmpt  5694  opeliunxp  5699  opeliun2xp  5700  xpundi  5701  elvvv  5708  opelinxp  5712  xpiindi  5792  elcnv2  5834  cnvuni  5843  dmuni  5871  brres  5953  dmres  5979  elidinxp  6011  restidsing  6020  elima3  6034  asymref  6081  imainss  6120  difxp  6130  xpdifid  6134  mptpreima  6204  coundir  6214  resco  6216  coass  6232  relrelss  6239  opreu2reurex  6260  dfpo2  6262  frpoind  6308  ordtri3or  6357  dffun2  6510  dffun6  6511  dffun3  6512  dffun4  6513  dffun5  6514  dffun6f  6515  dffun7  6527  dffun8  6528  dffun9  6529  svrelfun  6572  fncnv  6573  imadif  6584  dfmpt3  6634  fcnvres  6719  fint  6721  fin  6722  dff12  6737  fores  6764  dff1o4  6790  eqfnfv3  6987  fndmin  6999  fniniseg  7014  unpreima  7017  ffnfvf  7074  fsn2  7091  tpres  7157  fconstfv  7168  dff13f  7211  dff14a  7226  dff14b  7227  isocnv2  7287  f1opr  7424  eloprabga  7477  ffnov  7494  eqfnov  7497  foov  7542  uniuni  7717  tfindsg  7813  findsg  7849  funcnvuni  7884  opabex3d  7919  opabex3rd  7920  opabex3  7921  1stconst  8052  2ndconst  8053  frxp  8078  soxp  8081  xpord3lem  8101  suppvalbr  8116  suppofssd  8155  suppcoss  8159  mpoxopovel  8172  brtpos  8187  tpostpos  8198  dfsmo2  8289  dfrecs3  8314  rdglem1  8356  tz7.49  8386  brwitnlem  8444  oeeu  8541  naddasslem2  8633  brinxper  8675  erinxp  8740  mapsncnv  8843  cbvixp  8864  cbvixpv  8865  ixpin  8873  ixpiin  8874  mptelixpg  8885  elixpsn  8887  ixpsnf1o  8888  xpassen  9011  omxpenlem  9018  sbthcl  9039  sbthfilem  9134  wemapsolem  9467  dford2  9541  inf2  9544  zfinf  9560  ttrclselem2  9647  trcl  9649  frind  9674  frr3g  9680  iscard2  9900  leweon  9933  aceq1  10039  dfac3  10043  dfac4  10044  dfac5lem2  10046  dfac5  10051  kmlem3  10075  kmlem4  10076  kmlem14  10086  kmlem15  10087  dfackm  10089  infmap2  10139  fin23lem25  10246  zorn2lem7  10424  brdom6disj  10454  zfcndrep  10537  zfcndinf  10541  fpwwe  10569  axgroth4  10755  grothprim  10757  grothtsk  10758  nqpr  10937  addsrmo  10996  mulsrmo  10997  opelreal  11053  elnnz  12510  elznn0nn  12514  peano2uz2  12592  nnwos  12840  dflt2  13074  xmullem  13191  4fvwrd4  13576  preduz  13578  elfznelfzo  13701  fzind2  13716  fsuppmapnn0fiubex  13927  hashinfxadd  14320  hashgt23el  14359  hashfun  14372  fi1uzind  14442  brfi1uzind  14443  opfi1uzind  14446  cotr2g  14911  shftdm  15006  rexfiuz  15283  cbvsum  15630  cbvsumv  15631  mertenslem2  15820  mertens  15821  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  prodmo  15871  iprodmul  15938  divalglem10  16341  ndvdssub  16348  bitsmod  16375  algcvgblem  16516  isprm2  16621  isprm4  16623  hashdvds  16714  infpn2  16853  hashbc0  16945  xpscf  17498  funcpropd  17838  isffth2  17854  eldmcoa  18001  setcinv  18026  xpccatid  18123  yonedainv  18216  ispos  18249  ispos2  18250  joinfval2  18307  meetfval2  18321  istsr2  18519  isnsg2  19097  isnsg4  19108  isgim  19203  oppgid  19297  oppgcntz  19305  symgfix2  19357  efgval2  19665  iscyg2  19823  dmdprdd  19942  subgdmdprd  19977  issrg  20135  oppr1  20298  opprunit  20325  opprirred  20370  isrnghm  20389  isrhm  20426  issubrng  20492  subsubrng2  20509  subsubrg2  20544  rngcinv  20582  ringcinv  20616  isdomn2  20656  isdomn2OLD  20657  islmim  21026  lbsextg  21129  lidlnz  21209  resubdrg  21575  unocv  21647  pjfval2  21676  islinds2  21780  opsrtoslem1  22022  mdetunilem8  22575  istop2g  22852  isbasis2g  22904  tgval2  22912  isclo2  23044  isnrm2  23314  is1stc2  23398  llyi  23430  isfbas2  23791  elfg  23827  ufinffr  23885  isfcls  23965  alexsubALTlem2  24004  alexsubALTlem3  24005  cnextcn  24023  ustfilxp  24169  iscusp2  24257  metustid  24510  isclmp  25065  iscvsp  25096  tcphcph  25205  iscau3  25246  caucfil  25251  mdegleb  26037  ellogdm  26616  dvdsflsumcom  27166  logfac2  27196  dchrelbas3  27217  dchrvmasumlema  27479  nosupno  27683  noinfno  27698  noinfbnd1lem1  27703  dmcuts  27799  made0  27871  mulsproplem5  28128  norecdiv  28198  elnnzs  28409  uzsind  28413  zsoring  28417  legtrid  28675  outpasch  28839  axcontlem5  29053  axcontlem6  29054  axcontlem7  29055  nb3grpr2  29468  iscplgr  29500  dfpth2  29814  pthdlem1  29851  wwlksnextinj  29984  usgr2wspthon  30053  rusgrnumwwlkl1  30056  isclwwlk  30071  clwwlkccatlem  30076  clwwlknon2x  30190  iseupthf1o  30289  frcond3  30356  frgr3v  30362  4cycl2vnunb  30377  frgrncvvdeqlem2  30387  fusgr2wsp2nb  30421  numclwlk1lem1  30456  hhcms  31291  isch3  31329  ocsh  31371  pjhtheu  31482  pjpreeq  31486  h1deoi  31637  h1dei  31638  eleigvec  32045  cvbr2  32371  cvnbtwn2  32375  cvnbtwn4  32377  mdsl2i  32410  cvmdi  32412  mdsymlem6  32496  cdj3lem3b  32528  mo5f  32575  nmo  32576  rexunirn  32578  dmrab  32583  difrab2  32584  disjunsn  32681  unipreima  32733  dfcnv2  32765  1stpreima  32797  isunit2  33334  lsmsnorb2  33485  prmidl0  33543  ssmxidl  33567  1arithufdlem4  33640  ressply1mon1p  33661  extdgfialglem1  33870  zarcls  34052  rhmpreimacnlem  34062  isrnsiga  34291  rossros  34358  omsmeas  34501  eulerpartlemr  34552  eulerpartlemgvv  34554  ballotlemodife  34676  plymulx  34726  signstfvneq0  34750  bnj251  34879  bnj252  34880  bnj257  34884  bnj290  34887  bnj1304  34995  bnj153  35056  bnj543  35069  bnj571  35082  bnj580  35089  bnj607  35092  bnj882  35102  bnj964  35119  bnj996  35132  bnj1033  35145  bnj1176  35181  bnj1186  35183  bnj1189  35185  bnj1204  35188  bnj1253  35193  bnj1452  35228  bnj1463  35231  dff15  35261  axprALT2  35287  fineqvrep  35292  fineqvac  35294  lfuhgr3  35336  cusgredgex2  35339  usgrgt2cycl  35346  2cycl2d  35355  dfacycgr1  35360  erdszelem9  35415  cvmlift2lem9  35527  cvmlift2lem13  35531  satfvsucsuc  35581  satfdm  35585  satf0  35588  fmlasucdisj  35615  satffunlem  35617  satffunlem1lem1  35618  satffunlem2lem1  35620  elmthm  35792  axinfprim  35922  axacprim  35923  xpab  35942  dfso2  35971  dford5reg  35996  dfon2lem5  36001  dfon2  36006  brtxp2  36095  brpprod3a  36100  dfom5b  36126  brcart  36146  brimg  36151  funpartlem  36158  dfrecs2  36166  cgrxfr  36271  segletr  36330  sumeq2si  36418  prodeq2si  36420  cbvprodvw2  36463  trer  36532  fneval  36568  neifg  36587  df3nandALT1  36615  andnand1  36617  nandsym1  36638  weiunlem  36679  regsfromregtr  36690  bj-df-sb  36897  bj-eu3f  37089  bj-csbsnlem  37151  bj-snsetex  37211  bj-elsngl  37216  bj-snglc  37217  bj-restuni  37350  bj-dfmpoa  37371  bj-imdirco  37445  mptsnunlem  37593  icorempo  37606  isbasisrelowllem2  37611  relowlpssretop  37619  rdgeqoa  37625  difunieq  37629  dffinxpf  37640  nlpineqsn  37663  curf  37849  finixpnum  37856  ptrest  37870  poimirlem1  37872  poimirlem14  37885  poimirlem16  37887  poimirlem19  37890  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimir  37904  cnambfre  37919  itg2addnc  37925  ftc1anc  37952  opropabco  37975  isdrngo1  38207  keridl  38283  ispridlc  38321  selconj  38351  eldmres3  38534  eldmqsres  38544  cnvepres  38555  ecinn0  38604  alrmomorn  38609  moantr  38623  dfxrn2  38636  disjressuc2  38662  inxpxrn  38669  rnxrnres  38673  coss2cnvepres  38759  refrelredund4  38970  dferALTV2  39004  dfeldisj3  39062  dfpart2  39123  dfpeters2  39225  petseq  39227  prtlem70  39233  prtlem100  39235  prtlem15  39251  islshpat  39393  lcvbr2  39398  lcvbr3  39399  lcvnbtwn2  39403  ellkr  39465  cvrval2  39650  cvrnbtwn2  39651  cvrnbtwn3  39652  cvrnbtwn4  39655  ishlat2  39729  lplnexatN  39939  islvol5  39955  dath  40112  pclfinclN  40326  lhpexle3  40388  4atex2  40453  4atex2-0bOLDN  40455  isltrn2N  40496  cdleme0nex  40666  cdleme22b  40717  cdlemg17pq  41048  cdlemg19  41060  cdlemg21  41062  cdlemg33d  41085  dibopelvalN  41519  dibopelval2  41521  dib1dim  41541  dicelval2N  41558  diclspsn  41570  lcdlss  41995  mapd1o  42024  3factsumint2  42392  3factsumint3  42393  3factsumint  42395  hashnexinj  42498  sticksstones16  42532  sticksstones21  42537  unitscyglem3  42567  supinf  42612  fimgmcyclem  42903  eu6w  43034  mzpcompact2lem  43108  fz1eqin  43126  rexrabdioph  43151  expdiophlem1  43378  dford4  43386  fnwe2lem2  43408  fgraphopab  43560  dflim6  43621  onsucf1olem  43627  onsucrn  43628  nnoeomeqom  43669  faosnf0.11b  43783  ifpidg  43847  rp-fakeinunass  43871  rp-isfinite6  43874  dfsucon  43879  elinintrab  43933  elnonrel  43941  elmapintab  43952  dfrtrcl5  43985  imaiun1  44007  coiun1  44008  rfovcnvf1od  44360  andi3or  44380  uneqsn  44381  ntrneicls00  44445  rr-groth  44655  ismnushort  44657  rr-grothshortbi  44659  2sbc5g  44772  pm14.12  44777  2sb5nd  44916  uun2221  45168  uun2221p1  45169  uun2221p2  45170  2sb5ndVD  45265  2sb5ndALT  45287  modelaxreplem3  45336  iindif2f  45519  disjinfi  45551  climuz  46102  dfxlim2  46206  cncfshift  46232  dvnmul  46301  dvnprodlem2  46305  ismbl3  46344  ismbl4  46351  stoweidlem26  46384  stoweidlem35  46393  fourierdlem54  46518  fourierdlem83  46547  fourierdlem100  46564  fourierdlem104  46568  fourierdlem109  46573  fourierdlem112  46576  smfpimcc  47166  fcoresf1ob  47433  f1cof1b  47437  f1ocof1ob  47441  2reu8i  47473  dfdfat2  47488  ffnaov  47559  an4com24  47628  4an21  47630  iccpartiltu  47782  prproropf1olem0  47862  dfgric2  48275  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgprismgr4cycllem10  48464  grlimedgnedg  48491  2zrngmmgm  48612  rngcinvALTV  48636  ringcinvALTV  48670  pgrpgt2nabl  48726  islindeps  48813  lindslinindsimp1  48817  lindslinindsimp2  48823  ldepslinc  48869  blen1b  48948  coxp  49192  i0oii  49279  io1ii  49280  isthinc2  49779  isthinc3  49780  isthincd2  49796  istermc2  49834  istermc3  49835  dffun3f  50041  setrec1lem3  50048  elpglem3  50072  elpg  50073