Theorem anbi1i 625

Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi1i	⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32ri 575	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:  anbi2ci  626  bianbi  628  anandi  677  3an4anass  1105  3ioran  1106  4anpull2  1363  an33rean  1486  an42ds  1492  19.26-3an  1874  sb3an  2087  eeeanv  2355  sbel2x  2479  rexcomf  3277  cbvreu  3382  rabeqi  3403  rabrabi  3409  rabrab  3414  ceqsex3v  3484  spc2ed  3544  rexrab  3643  reurab  3648  rmo3f  3681  reuind  3700  rmo3  3828  ssrab  4012  rexun  4137  elin3  4147  inass  4169  rexin  4191  dfun2  4211  inrab2  4258  rabun2  4265  reuun2  4266  undif4  4408  rexdifpr  4604  rexsns  4616  rexdifsn  4738  2ralunsn  4839  iuncom4  4943  iindif1  5018  iunxiun  5040  disjxun  5084  zfrep4  5229  inuni  5288  reusv2lem4  5339  reusv2  5341  otth2  5432  copsexgw  5439  copsexg  5440  copsex2g  5442  copsex4g  5444  vopelopabsb  5478  rabxp  5673  opeliunxp  5692  opeliun2xp  5693  xpundir  5695  xpiundi  5696  xpiundir  5697  brinxp2  5703  copsex2gb  5756  cnvopab  6095  dminss  6112  imainss  6113  difxp  6123  cnvresima  6189  coundi  6206  resco  6209  imaco  6210  rnco  6211  rncoOLD  6212  coiun  6216  coi1  6222  coass  6225  cnvpo  6246  xpco  6248  dfpo2  6255  frpoind  6301  dffun2  6503  fncnv  6566  imadif  6577  mptun  6639  ffrnb  6677  dff1o2  6780  dff1o3  6781  brprcneu  6825  brprcneuALT  6826  fvun2  6927  eqfnfv3  6980  respreima  7013  f1ompt  7058  f1ossf1o  7076  fsn  7083  fmptsng  7117  fmptsnd  7118  tpres  7150  abrexco  7193  imaiun  7194  f1mpt  7210  dff1o6  7224  imaeqsexvOLD  7312  riotarab  7360  oprabidw  7392  oprabid  7393  dfoprab2  7419  oprab4  7447  mpomptx  7474  elpwpwel  7715  elxp4  7867  elxp5  7868  ffoss  7893  f11o  7894  opabex3d  7912  opabex3rd  7913  opabex3  7914  abexssex  7917  elxp7  7971  dfopab2  7999  dfoprab3s  8000  fsplit  8061  frxp  8070  xporderlem  8071  frpoins3xp3g  8085  soseq  8103  suppssov1  8141  suppssov2  8142  suppssfv  8146  brtpos2  8176  tpostpos  8190  tposmpo  8207  dfrecs3  8306  oarec  8491  oeeu  8533  eldifsucnn  8594  naddasslem1  8624  mapsncnv  8835  dfixp  8841  domen  8902  xpsnen  8993  xpcomco  8999  xpassen  9003  sbthlem9  9027  frfi  9189  marypha2lem2  9343  brttrcl2  9629  epfrs  9646  tcsni  9656  frind  9668  cp  9809  dfac5lem1  10039  dfac5lem2  10040  dfac5lem5  10043  kmlem3  10069  dfackm  10083  cfval2  10176  cflim3  10178  cfss  10181  cfslb  10182  zfcndrep  10531  eltsk2g  10668  ltexpi  10819  recmulnq  10881  ltexprlem4  10956  addsrpr  10992  mulsrpr  10993  addcnsr  11052  mulcnsr  11053  ltresr  11057  axrrecex  11080  elnnz  12528  elnn0z  12531  fnn0ind  12622  rexuz2  12843  rexrp  12959  elixx3g  13305  elfz2  13462  elfzuzb  13466  fznn  13540  elfz2nn0  13566  fznn0  13567  4fvwrd4  13596  preduz  13598  elfzo2  13610  fzind2  13737  hashgt23el  14380  hashf1lem1  14411  hashf1lem2  14412  fz1isolem  14417  s4f1o  14874  wwlktovfo  14914  fsum2dlem  15726  modfsummod  15751  prodeq1i  15875  sinltx  16150  divalglem10  16365  divalgb  16367  coprmproddvdslem  16625  isprm2  16645  infpn2  16878  prdsle  17419  prdsless  17420  prdsleval  17434  imasleval  17499  xpscf  17523  dfiso2  17733  oppcsect  17739  elhoma  17993  ispos2  18275  lubeldm  18311  glbeldm  18324  tosso  18377  ismgmhm  18658  issubmgm  18664  submgmacs  18679  ismhm  18747  issubm  18765  submacs  18789  issubg  19096  issubg3  19114  gaorb  19276  pmtrrn2  19429  efgcpbllema  19723  efgcpbllemb  19724  frgpuplem  19741  imasabl  19845  subgdmdprd  20005  dprd2d2  20015  omndmul2  20102  dfrhm2  20448  opprnzrb  20492  issubrg  20542  isdomn3  20686  drngprop  20715  drngid2  20723  opprdrng  20735  isabv  20782  isorng  20832  islss  20923  islbs  21066  lsmspsn  21074  isobs  21713  islinds  21802  isassa  21849  aspval2  21891  ltbval  22034  opsrle  22038  opsrtoslem1  22046  fvmptnn04if  22827  ntreq0  23055  restntr  23160  cnnei  23260  hausnei2  23331  cmpcov2  23368  cmpsub  23378  uncmp  23381  cmpfi  23386  llyi  23452  dissnlocfin  23507  iskgen3  23527  1stckgenlem  23531  ptpjpre1  23549  txcnpi  23586  txtube  23618  hausdiag  23623  txlm  23626  txkgen  23630  cfinfil  23871  csdfil  23872  supfil  23873  fin1aufil  23910  elflim2  23942  hauspwpwf1  23965  txflf  23984  isfcls  23987  alexsubALTlem3  24027  alexsubALT  24029  cnextcn  24045  istmd  24052  istgp  24055  tgphaus  24095  qustgplem  24099  istrg  24142  istdrg  24144  istlm  24163  blres  24409  isms2  24428  metrest  24502  metuel2  24543  restmetu  24548  isngp  24574  isnlm  24653  elii1  24915  isclmp  25077  iscvsp  25108  isncvsngp  25129  iscph  25150  cfilucfil3  25300  isbn  25318  limcrcl  25854  ig1pval3  26156  plydivex  26277  ellogdm  26619  cubic  26829  dmarea  26937  vmasum  27196  lgsquadlem1  27360  lgsquadlem2  27361  elno3  27636  lenlts  27733  madeval2  27842  elnnzs  28410  istrkg3ld  28546  legov  28670  ltgov  28682  colinearalg  28996  axeuclid  29049  axcontlem2  29051  axcontlem5  29054  nbgrel  29426  nbupgrres  29450  nbusgredgeu0  29454  nb3grprlem2  29467  nb3grpr2  29469  nb3gr2nb  29470  cplgr3v  29521  finsumvtxdg2ssteplem3  29634  wlkonprop  29743  upgrtrls  29786  upgristrl  29787  wksonproplem  29789  usgr2pth0  29851  wwlksnext  29979  wwlksnextsurj  29986  wwlksnfi  29992  wspthsnwspthsnon  30002  wpthswwlks2on  30050  rusgrnumwwlkl1  30057  erclwwlkref  30108  isclwwlknx  30124  clwwlknwwlksn  30126  clwwlkel  30134  erclwwlknref  30157  clwlknf1oclwwlkn  30172  clwwlknonel  30183  clwwlknon1  30185  clwwlknon2x  30191  clwwlkvbij  30201  iseupthf1o  30290  2pthfrgrrn  30370  fusgr2wsp2nb  30422  numclwwlk1lem2f1  30445  numclwwlkovh  30461  numclwlk2lem2f1o  30467  frgrregord013  30483  avril1  30551  islno  30842  h2hlm  31069  hcau  31273  hhsssh2  31359  dfch2  31496  elcnop  31946  ellnop  31947  elhmop  31962  elcnfn  31971  ellnfn  31972  dmadjss  31976  adjeu  31978  adjval  31979  hhcno  31993  hhcnf  31994  eleigvec  32046  isst  32302  ishst  32303  cvnbtwn3  32377  cvnbtwn4  32378  chirredi  32483  sumdmdii  32504  an52ds  32539  an62ds  32540  an72ds  32541  an82ds  32542  or3di  32546  rexunirn  32579  rmoun  32581  dmrab  32584  difrab2  32585  iunin1f  32645  disjunsn  32682  opeldifid  32687  ofpreima  32756  mpomptxf  32769  fdifsupp  32776  1stpreima  32798  2ndpreima  32799  f1od2  32810  resf1o  32821  maprnin  32822  nndiffz1  32877  ismnt  33061  mgcval  33065  erler  33344  opprnsg  33562  1arithidom  33615  1arithufdlem4  33625  extdgfialglem1  33855  smatrcl  33959  ordtconnlem1  34087  isrrext  34163  sigaex  34273  sigaval  34274  omssubaddlem  34462  omssubadd  34463  eulerpartleme  34526  eulerpartlemt0  34532  eulerpartlemr  34537  eulerpartlemn  34544  probun  34582  ballotlemelo  34651  ballotlem2  34652  ballotlemfc0  34656  ballotlemfcc  34657  reprdifc  34790  bnj248  34862  bnj250  34863  bnj268  34871  bnj312  34874  bnj945  34935  bnj110  35019  bnj849  35086  bnj882  35087  bnj893  35089  bnj916  35094  bnj983  35112  bnj1040  35133  bnj1175  35165  cusgredgex  35323  cusgr3cyclex  35337  erdszelem1  35392  iscvm  35460  elmpst  35737  mpstrcl  35742  dfso3  35921  xpab  35927  coepr  35954  dfdm5  35974  dfrn5  35975  elima4  35977  fv1stcnv  35978  fv2ndcnv  35979  brpprod  36084  dfon3  36091  elfix  36102  dffix2  36104  elfuns  36114  brimg  36136  brapply  36137  lemsuccf  36140  funpartlem  36143  funpartfun  36144  brrestrict  36150  dfrecs2  36151  dfrdg4  36152  lineunray  36348  ellines  36353  rmoeqi  36388  reueqi  36390  itgeq12i  36407  finminlem  36519  fneval  36553  neibastop3  36563  eliminable-abelv  37195  bj-inrab  37253  bj-axseprep  37400  bj-rest10  37419  bj-restpw  37423  bj-restuni  37428  bj-mpomptALT  37450  copsex2gd  37471  bj-imdirco  37523  icorempo  37684  isbasisrelowllem1  37688  isbasisrelowllem2  37689  relowlpssretop  37697  pibt2  37750  wl-ifp-ncond2  37798  wl-df3-3mintru2  37819  wl-2mintru1  37823  rabiun  37931  iundif1  37932  lindsenlbs  37953  poimirlem4  37962  poimirlem25  37983  poimirlem26  37984  poimirlem29  37987  poimirlem30  37988  ismblfin  37999  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  itg2addnclem2  38010  itg2addnclem3  38011  itg2addnc  38012  ftc1anc  38039  isbnd2  38121  bndss  38124  heibor1lem  38147  heibor1  38148  isrngohom  38303  isidl  38352  sbccom2lem  38462  anan  38573  eqbrb  38577  eqelb  38579  br1cnvinxp  38597  eldmqsres  38631  idinxpssinxp2  38662  moantr  38710  inxpxrn  38756  blockadjliftmap  38796  dfcoss3  38842  cocossss  38864  ressn2  38870  br1cossinidres  38877  br1cossincnvepres  38878  br1cossxrnidres  38879  br1cossxrncnvepres  38880  refrelcoss2  38892  symrelcoss2  38894  cosscnvssid5  38906  br1cossxrncnvssrres  38926  dfrefrel3  38934  dfcnvrefrel3  38949  cosselcnvrefrels2  38956  cosselcnvrefrels3  38957  cosselcnvrefrels4  38958  cosselcnvrefrels5  38959  dfsymrel3  38972  refsymrel2  38989  refsymrel3  38990  elrefsymrels3  38992  dftrrel3  39000  dfeqvrel2  39012  dfeqvrel3  39013  redundpbi1  39053  refrelredund3  39059  eldmqs1cossres  39082  dffunALTV2  39111  dffunALTV3  39112  dffunALTV4  39113  dffunALTV5  39114  dfdisjALTV  39136  dfdisjALTV2  39137  dfdisjALTV3  39138  dfdisjALTV4  39139  disjimdmqseq  39147  eldisjs3  39159  eldisjs4  39160  disjsuc  39197  prtlem70  39320  prtlem100  39322  prter2  39344  lsateln0  39458  islshpat  39480  lcvnbtwn3  39491  islfl  39523  ishlat1  39815  ishlat2  39816  cvrat4  39906  islvol5  40042  psubspset  40207  snatpsubN  40213  dalawlem13  40346  psubclsetN  40399  isltrn2N  40583  cdlemftr3  41028  dibelval3  41610  dicval2  41642  dicopelval2  41644  dicelval2N  41645  dihglb2  41805  islpolN  41946  lcfls1c  41999  mapdvalc  42092  mapdval4N  42095  mapdordlem1a  42097  aks4d1p8  42543  fimgmcyc  42996  prjsperref  43056  prjspeclsp  43062  elmzpcl  43175  mzpindd  43195  fphpd  43265  pw2f1ocnv  43486  islmodfg  43518  islssfg2  43520  dflim6  43713  onsucf1olem  43719  omge2  43747  tfsconcatlem  43785  tfsconcat0i  43794  rp-isfinite6  43966  minregex  43982  elmapintrab  44024  elinintrab  44025  relintab  44031  dfrtrcl5  44077  fsovrfovd  44457  ntrk1k3eqk13  44498  gneispace3  44581  k0004lem1  44595  pm13.192  44858  opelopab4  44999  ax6e2nd  45006  en3lplem2VD  45291  ax6e2ndVD  45355  ax6e2ndALT  45377  permaxrep  45454  iuneq1i  45536  ssrabf  45565  limcrecl  46080  dvnprodlem2  46396  fourierdlem103  46658  fourierdlem104  46659  4an21  47733  sprvalpwn0  47958  pairreueq  47985  dfvopnbgr2  48344  isubgredg  48357  xpsnopab  48648  sgrp2sgrp  48719  mpomptx2  48826  lindslinindsimp1  48948  lindslinindsimp2  48954  itsclc0b  49263  mo0sn  49306  coxp  49323  isthincd2  49927  thinccic  49961  2arwcatlem1  50085  setc1onsubc  50092  alsconv  50280  aacllem  50291