Theorem anbi1i 624

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  625  bianbi  627  anandi  676  3an4anass  1105  3ioran  1106  4anpull2  1362  an6  1447  an33rean  1485  19.26-3an  1872  sb3an  2081  eeeanv  2352  sbel2x  2479  rexcomf  3303  cbvreuwOLD  3415  cbvreu  3428  rabeqi  3450  rabrabi  3456  rabrab  3461  ceqsex3v  3537  spc2ed  3601  rexabOLD  3701  rexrab  3702  reurab  3707  rmo3f  3740  reuind  3759  rmo3  3889  ssrab  4073  rexun  4196  elin3  4206  inass  4228  rexin  4250  dfun2  4270  inrab2  4317  rabun2  4324  reuun2  4325  undif4  4467  rexdifpr  4659  rexsns  4671  rexdifsn  4794  2ralunsn  4895  iuncom4  5000  iindif1  5075  iunxiun  5097  disjxun  5141  zfrep4  5293  inuni  5350  reusv2lem4  5401  reusv2  5403  otth2  5488  copsexgw  5495  copsexg  5496  copsex2g  5498  copsex4g  5500  vopelopabsb  5534  rabxp  5733  opeliunxp  5752  opeliun2xp  5753  xpundir  5755  xpiundi  5756  xpiundir  5757  brinxp2  5763  copsex2gb  5816  cnvopab  6157  dminss  6173  imainss  6174  difxp  6184  cnvresima  6250  coundi  6267  resco  6270  imaco  6271  rnco  6272  coiun  6276  coi1  6282  coass  6285  cnvpo  6307  xpco  6309  dfpo2  6316  frpoind  6363  wfiOLD  6372  dffun2  6571  dffun2OLD  6572  dffun2OLDOLD  6573  fncnv  6639  imadif  6650  mptun  6714  ffrnb  6750  dff1o2  6853  dff1o3  6854  brprcneu  6896  brprcneuALT  6897  fvun2  7001  eqfnfv3  7053  respreima  7086  f1ompt  7131  f1ossf1o  7148  fsn  7155  fmptsng  7188  fmptsnd  7189  tpres  7221  abrexco  7264  imaiun  7265  f1mpt  7281  dff1o6  7295  imaeqsexvOLD  7383  riotarab  7430  oprabidw  7462  oprabid  7463  dfoprab2  7491  oprab4  7519  mpomptx  7546  elpwpwel  7787  elxp4  7944  elxp5  7945  ffoss  7970  f11o  7971  opabex3d  7990  opabex3rd  7991  opabex3  7992  abexssex  7995  elxp7  8049  dfopab2  8077  dfoprab3s  8078  fsplit  8142  frxp  8151  xporderlem  8152  frpoins3xp3g  8166  soseq  8184  suppssov1  8222  suppssov2  8223  suppssfv  8227  brtpos2  8257  tpostpos  8271  tposmpo  8288  wfrfunOLD  8359  dfrecs3  8412  dfrecs3OLD  8413  oarec  8600  oeeu  8641  eldifsucnn  8702  naddasslem1  8732  mapsncnv  8933  dfixp  8939  domen  9002  xpsnen  9095  xpcomco  9102  xpassen  9106  sbthlem9  9131  frfi  9321  marypha2lem2  9476  brttrcl2  9754  epfrs  9771  tcsni  9783  frind  9790  cp  9931  dfac5lem1  10163  dfac5lem2  10164  dfac5lem5  10167  kmlem3  10193  dfackm  10207  cfval2  10300  cflim3  10302  cfss  10305  cfslb  10306  zfcndrep  10654  eltsk2g  10791  ltexpi  10942  recmulnq  11004  ltexprlem4  11079  addsrpr  11115  mulsrpr  11116  addcnsr  11175  mulcnsr  11176  ltresr  11180  axrrecex  11203  elnnz  12623  elnn0z  12626  fnn0ind  12717  rexuz2  12941  rexrp  13056  elixx3g  13400  elfz2  13554  elfzuzb  13558  fznn  13632  elfz2nn0  13658  fznn0  13659  4fvwrd4  13688  preduz  13690  elfzo2  13702  fzind2  13824  hashgt23el  14463  hashf1lem1  14494  hashf1lem2  14495  fz1isolem  14500  s4f1o  14957  wwlktovfo  14997  fsum2dlem  15806  modfsummod  15830  prodeq1i  15952  sinltx  16225  divalglem10  16439  divalgb  16441  coprmproddvdslem  16699  isprm2  16719  infpn2  16951  prdsle  17507  prdsless  17508  prdsleval  17522  imasleval  17586  xpscf  17610  dfiso2  17816  oppcsect  17822  elhoma  18077  ispos2  18361  lubeldm  18398  glbeldm  18411  tosso  18464  ismgmhm  18709  issubmgm  18715  submgmacs  18730  ismhm  18798  issubm  18816  submacs  18840  issubg  19144  issubg3  19162  gaorb  19325  pmtrrn2  19478  efgcpbllema  19772  efgcpbllemb  19773  frgpuplem  19790  imasabl  19894  subgdmdprd  20054  dprd2d2  20064  dfrhm2  20474  opprnzrb  20521  issubrg  20571  isdomn3  20715  drngprop  20744  drngid2  20752  opprdrng  20764  isabv  20812  islss  20932  islbs  21075  lsmspsn  21083  isobs  21740  islinds  21829  isassa  21876  aspval2  21918  ltbval  22061  opsrle  22065  opsrtoslem1  22079  fvmptnn04if  22855  ntreq0  23085  restntr  23190  cnnei  23290  hausnei2  23361  cmpcov2  23398  cmpsub  23408  uncmp  23411  cmpfi  23416  llyi  23482  dissnlocfin  23537  iskgen3  23557  1stckgenlem  23561  ptpjpre1  23579  txcnpi  23616  txtube  23648  hausdiag  23653  txlm  23656  txkgen  23660  cfinfil  23901  csdfil  23902  supfil  23903  fin1aufil  23940  elflim2  23972  hauspwpwf1  23995  txflf  24014  isfcls  24017  alexsubALTlem3  24057  alexsubALT  24059  cnextcn  24075  istmd  24082  istgp  24085  tgphaus  24125  qustgplem  24129  istrg  24172  istdrg  24174  istlm  24193  blres  24441  isms2  24460  metrest  24537  metuel2  24578  restmetu  24583  isngp  24609  isnlm  24696  elii1  24964  isclmp  25130  iscvsp  25161  isncvsngp  25183  iscph  25204  cfilucfil3  25354  isbn  25372  limcrcl  25909  ig1pval3  26217  plydivex  26339  ellogdm  26681  cubic  26892  dmarea  27000  vmasum  27260  lgsquadlem1  27424  lgsquadlem2  27425  elno3  27700  slenlt  27797  madeval2  27892  elnnzs  28387  istrkg3ld  28469  legov  28593  ltgov  28605  colinearalg  28925  axeuclid  28978  axcontlem2  28980  axcontlem5  28983  nbgrel  29357  nbupgrres  29381  nbusgredgeu0  29385  nb3grprlem2  29398  nb3grpr2  29400  nb3gr2nb  29401  cplgr3v  29452  finsumvtxdg2ssteplem3  29565  wlkonprop  29676  upgrtrls  29719  upgristrl  29720  wksonproplem  29722  wksonproplemOLD  29723  usgr2pth0  29785  wwlksnext  29913  wwlksnextsurj  29920  wwlksnfi  29926  wspthsnwspthsnon  29936  wpthswwlks2on  29981  rusgrnumwwlkl1  29988  erclwwlkref  30039  isclwwlknx  30055  clwwlknwwlksn  30057  clwwlkel  30065  erclwwlknref  30088  clwlknf1oclwwlkn  30103  clwwlknonel  30114  clwwlknon1  30116  clwwlknon2x  30122  clwwlkvbij  30132  iseupthf1o  30221  2pthfrgrrn  30301  fusgr2wsp2nb  30353  numclwwlk1lem2f1  30376  numclwwlkovh  30392  numclwlk2lem2f1o  30398  frgrregord013  30414  avril1  30482  islno  30772  h2hlm  30999  hcau  31203  hhsssh2  31289  dfch2  31426  elcnop  31876  ellnop  31877  elhmop  31892  elcnfn  31901  ellnfn  31902  dmadjss  31906  adjeu  31908  adjval  31909  hhcno  31923  hhcnf  31924  eleigvec  31976  isst  32232  ishst  32233  cvnbtwn3  32307  cvnbtwn4  32308  chirredi  32413  sumdmdii  32434  an42ds  32469  an52ds  32470  an62ds  32471  an72ds  32472  an82ds  32473  or3di  32478  rexunirn  32511  rmoun  32513  dmrab  32516  difrab2  32517  iunin1f  32570  disjunsn  32607  opeldifid  32612  ofpreima  32675  mpomptxf  32687  fdifsupp  32694  1stpreima  32716  2ndpreima  32717  f1od2  32732  resf1o  32741  maprnin  32742  nndiffz1  32788  ismnt  32973  mgcval  32977  omndmul2  33089  erler  33269  isorng  33329  opprnsg  33512  1arithidom  33565  1arithufdlem4  33575  smatrcl  33795  ordtconnlem1  33923  isrrext  34001  sigaex  34111  sigaval  34112  omssubaddlem  34301  omssubadd  34302  eulerpartleme  34365  eulerpartlemt0  34371  eulerpartlemr  34376  eulerpartlemn  34383  probun  34421  ballotlemelo  34490  ballotlem2  34491  ballotlemfc0  34495  ballotlemfcc  34496  reprdifc  34642  bnj248  34714  bnj250  34715  bnj268  34723  bnj312  34726  bnj945  34787  bnj110  34872  bnj849  34939  bnj882  34940  bnj893  34942  bnj916  34947  bnj983  34965  bnj1040  34986  bnj1175  35018  cusgredgex  35127  cusgr3cyclex  35141  erdszelem1  35196  iscvm  35264  elmpst  35541  mpstrcl  35546  dfso3  35720  xpab  35726  coepr  35753  dfdm5  35773  dfrn5  35774  elima4  35776  fv1stcnv  35777  fv2ndcnv  35778  brpprod  35886  dfon3  35893  elfix  35904  dffix2  35906  elfuns  35916  brimg  35938  brapply  35939  brsuccf  35942  funpartlem  35943  funpartfun  35944  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  lineunray  36148  ellines  36153  rmoeqi  36188  reueqi  36190  itgeq12i  36207  finminlem  36319  fneval  36353  neibastop3  36363  eliminable-abelv  36870  bj-inrab  36928  bj-rest10  37089  bj-restpw  37093  bj-restuni  37098  bj-mpomptALT  37120  bj-imdirco  37191  icorempo  37352  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlpssretop  37365  pibt2  37418  wl-ifp-ncond2  37466  wl-df3-3mintru2  37487  wl-2mintru1  37491  rabiun  37600  iundif1  37601  lindsenlbs  37622  poimirlem4  37631  poimirlem25  37652  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem2  37679  itg2addnclem3  37680  itg2addnc  37681  ftc1anc  37708  isbnd2  37790  bndss  37793  heibor1lem  37816  heibor1  37817  isrngohom  37972  isidl  38021  sbccom2lem  38131  anan  38230  eqbrb  38234  eqelb  38236  br1cnvinxp  38257  eldmqsres  38288  idinxpssinxp2  38319  moantr  38365  inxpxrn  38396  dfcoss3  38415  cocossss  38437  ressn2  38443  br1cossinidres  38450  br1cossincnvepres  38451  br1cossxrnidres  38452  br1cossxrncnvepres  38453  refrelcoss2  38465  symrelcoss2  38467  cosscnvssid5  38479  br1cossxrncnvssrres  38509  dfrefrel3  38517  dfcnvrefrel3  38532  cosselcnvrefrels2  38539  cosselcnvrefrels3  38540  cosselcnvrefrels4  38541  cosselcnvrefrels5  38542  dfsymrel3  38551  refsymrel2  38568  refsymrel3  38569  elrefsymrels3  38571  dftrrel3  38579  dfeqvrel2  38591  dfeqvrel3  38592  redundpbi1  38632  refrelredund3  38638  eldmqs1cossres  38660  dffunALTV2  38689  dffunALTV3  38690  dffunALTV4  38691  dffunALTV5  38692  dfdisjALTV  38714  dfdisjALTV2  38715  dfdisjALTV3  38716  dfdisjALTV4  38717  eldisjs3  38725  eldisjs4  38726  disjsuc  38760  prtlem70  38858  prtlem100  38860  prter2  38882  lsateln0  38996  islshpat  39018  lcvnbtwn3  39029  islfl  39061  ishlat1  39353  ishlat2  39354  cvrat4  39445  islvol5  39581  psubspset  39746  snatpsubN  39752  dalawlem13  39885  psubclsetN  39938  isltrn2N  40122  cdlemftr3  40567  dibelval3  41149  dicval2  41181  dicopelval2  41183  dicelval2N  41184  dihglb2  41344  islpolN  41485  lcfls1c  41538  mapdvalc  41631  mapdval4N  41634  mapdordlem1a  41636  aks4d1p8  42088  fimgmcyc  42544  prjsperref  42616  prjspeclsp  42622  elmzpcl  42737  mzpindd  42757  fphpd  42827  pw2f1ocnv  43049  islmodfg  43081  islssfg2  43083  dflim6  43277  onsucf1olem  43283  omge2  43311  tfsconcatlem  43349  tfsconcat0i  43358  rp-isfinite6  43531  minregex  43547  elmapintrab  43589  elinintrab  43590  relintab  43596  dfrtrcl5  43642  fsovrfovd  44022  ntrk1k3eqk13  44063  gneispace3  44146  k0004lem1  44160  pm13.192  44429  opelopab4  44571  ax6e2nd  44578  en3lplem2VD  44864  ax6e2ndVD  44928  ax6e2ndALT  44950  iuneq1i  45090  ssrabf  45119  limcrecl  45644  dvnprodlem2  45962  fourierdlem103  46224  fourierdlem104  46225  4an21  47282  sprvalpwn0  47470  pairreueq  47497  dfvopnbgr2  47839  isubgredg  47852  xpsnopab  48073  sgrp2sgrp  48144  mpomptx2  48251  lindslinindsimp1  48374  lindslinindsimp2  48380  itsclc0b  48693  mo0sn  48735  coxp  48744  isthincd2  49086  thinccic  49118  alsconv  49309  aacllem  49320