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  1104  3ioran  1105  4anpull2  1362  an33rean  1485  19.26-3an  1872  sb3an  2082  eeeanv  2348  sbel2x  2473  rexcomf  3279  cbvreuwOLD  3389  cbvreu  3400  rabeqi  3422  rabrabi  3428  rabrab  3433  ceqsex3v  3506  spc2ed  3570  rexrab  3670  reurab  3675  rmo3f  3708  reuind  3727  rmo3  3855  ssrab  4039  rexun  4162  elin3  4172  inass  4194  rexin  4216  dfun2  4236  inrab2  4283  rabun2  4290  reuun2  4291  undif4  4433  rexdifpr  4626  rexsns  4638  rexdifsn  4761  2ralunsn  4862  iuncom4  4967  iindif1  5042  iunxiun  5064  disjxun  5108  zfrep4  5251  inuni  5308  reusv2lem4  5359  reusv2  5361  otth2  5446  copsexgw  5453  copsexg  5454  copsex2g  5456  copsex4g  5458  vopelopabsb  5492  rabxp  5689  opeliunxp  5708  opeliun2xp  5709  xpundir  5711  xpiundi  5712  xpiundir  5713  brinxp2  5719  copsex2gb  5772  cnvopab  6113  dminss  6129  imainss  6130  difxp  6140  cnvresima  6206  coundi  6223  resco  6226  imaco  6227  rnco  6228  coiun  6232  coi1  6238  coass  6241  cnvpo  6263  xpco  6265  dfpo2  6272  frpoind  6318  dffun2  6524  dffun2OLD  6525  dffun2OLDOLD  6526  fncnv  6592  imadif  6603  mptun  6667  ffrnb  6705  dff1o2  6808  dff1o3  6809  brprcneu  6851  brprcneuALT  6852  fvun2  6956  eqfnfv3  7008  respreima  7041  f1ompt  7086  f1ossf1o  7103  fsn  7110  fmptsng  7145  fmptsnd  7146  tpres  7178  abrexco  7221  imaiun  7222  f1mpt  7239  dff1o6  7253  imaeqsexvOLD  7341  riotarab  7389  oprabidw  7421  oprabid  7422  dfoprab2  7450  oprab4  7478  mpomptx  7505  elpwpwel  7746  elxp4  7901  elxp5  7902  ffoss  7927  f11o  7928  opabex3d  7947  opabex3rd  7948  opabex3  7949  abexssex  7952  elxp7  8006  dfopab2  8034  dfoprab3s  8035  fsplit  8099  frxp  8108  xporderlem  8109  frpoins3xp3g  8123  soseq  8141  suppssov1  8179  suppssov2  8180  suppssfv  8184  brtpos2  8214  tpostpos  8228  tposmpo  8245  dfrecs3  8344  oarec  8529  oeeu  8570  eldifsucnn  8631  naddasslem1  8661  mapsncnv  8869  dfixp  8875  domen  8936  xpsnen  9029  xpcomco  9036  xpassen  9040  sbthlem9  9065  frfi  9239  marypha2lem2  9394  brttrcl2  9674  epfrs  9691  tcsni  9703  frind  9710  cp  9851  dfac5lem1  10083  dfac5lem2  10084  dfac5lem5  10087  kmlem3  10113  dfackm  10127  cfval2  10220  cflim3  10222  cfss  10225  cfslb  10226  zfcndrep  10574  eltsk2g  10711  ltexpi  10862  recmulnq  10924  ltexprlem4  10999  addsrpr  11035  mulsrpr  11036  addcnsr  11095  mulcnsr  11096  ltresr  11100  axrrecex  11123  elnnz  12546  elnn0z  12549  fnn0ind  12640  rexuz2  12865  rexrp  12981  elixx3g  13326  elfz2  13482  elfzuzb  13486  fznn  13560  elfz2nn0  13586  fznn0  13587  4fvwrd4  13616  preduz  13618  elfzo2  13630  fzind2  13753  hashgt23el  14396  hashf1lem1  14427  hashf1lem2  14428  fz1isolem  14433  s4f1o  14891  wwlktovfo  14931  fsum2dlem  15743  modfsummod  15767  prodeq1i  15889  sinltx  16164  divalglem10  16379  divalgb  16381  coprmproddvdslem  16639  isprm2  16659  infpn2  16891  prdsle  17432  prdsless  17433  prdsleval  17447  imasleval  17511  xpscf  17535  dfiso2  17741  oppcsect  17747  elhoma  18001  ispos2  18283  lubeldm  18319  glbeldm  18332  tosso  18385  ismgmhm  18630  issubmgm  18636  submgmacs  18651  ismhm  18719  issubm  18737  submacs  18761  issubg  19065  issubg3  19083  gaorb  19246  pmtrrn2  19397  efgcpbllema  19691  efgcpbllemb  19692  frgpuplem  19709  imasabl  19813  subgdmdprd  19973  dprd2d2  19983  dfrhm2  20390  opprnzrb  20437  issubrg  20487  isdomn3  20631  drngprop  20660  drngid2  20668  opprdrng  20680  isabv  20727  islss  20847  islbs  20990  lsmspsn  20998  isobs  21636  islinds  21725  isassa  21772  aspval2  21814  ltbval  21957  opsrle  21961  opsrtoslem1  21969  fvmptnn04if  22743  ntreq0  22971  restntr  23076  cnnei  23176  hausnei2  23247  cmpcov2  23284  cmpsub  23294  uncmp  23297  cmpfi  23302  llyi  23368  dissnlocfin  23423  iskgen3  23443  1stckgenlem  23447  ptpjpre1  23465  txcnpi  23502  txtube  23534  hausdiag  23539  txlm  23542  txkgen  23546  cfinfil  23787  csdfil  23788  supfil  23789  fin1aufil  23826  elflim2  23858  hauspwpwf1  23881  txflf  23900  isfcls  23903  alexsubALTlem3  23943  alexsubALT  23945  cnextcn  23961  istmd  23968  istgp  23971  tgphaus  24011  qustgplem  24015  istrg  24058  istdrg  24060  istlm  24079  blres  24326  isms2  24345  metrest  24419  metuel2  24460  restmetu  24465  isngp  24491  isnlm  24570  elii1  24838  isclmp  25004  iscvsp  25035  isncvsngp  25056  iscph  25077  cfilucfil3  25227  isbn  25245  limcrcl  25782  ig1pval3  26090  plydivex  26212  ellogdm  26555  cubic  26766  dmarea  26874  vmasum  27134  lgsquadlem1  27298  lgsquadlem2  27299  elno3  27574  slenlt  27671  madeval2  27768  elnnzs  28296  istrkg3ld  28395  legov  28519  ltgov  28531  colinearalg  28844  axeuclid  28897  axcontlem2  28899  axcontlem5  28902  nbgrel  29274  nbupgrres  29298  nbusgredgeu0  29302  nb3grprlem2  29315  nb3grpr2  29317  nb3gr2nb  29318  cplgr3v  29369  finsumvtxdg2ssteplem3  29482  wlkonprop  29593  upgrtrls  29636  upgristrl  29637  wksonproplem  29639  wksonproplemOLD  29640  usgr2pth0  29702  wwlksnext  29830  wwlksnextsurj  29837  wwlksnfi  29843  wspthsnwspthsnon  29853  wpthswwlks2on  29898  rusgrnumwwlkl1  29905  erclwwlkref  29956  isclwwlknx  29972  clwwlknwwlksn  29974  clwwlkel  29982  erclwwlknref  30005  clwlknf1oclwwlkn  30020  clwwlknonel  30031  clwwlknon1  30033  clwwlknon2x  30039  clwwlkvbij  30049  iseupthf1o  30138  2pthfrgrrn  30218  fusgr2wsp2nb  30270  numclwwlk1lem2f1  30293  numclwwlkovh  30309  numclwlk2lem2f1o  30315  frgrregord013  30331  avril1  30399  islno  30689  h2hlm  30916  hcau  31120  hhsssh2  31206  dfch2  31343  elcnop  31793  ellnop  31794  elhmop  31809  elcnfn  31818  ellnfn  31819  dmadjss  31823  adjeu  31825  adjval  31826  hhcno  31840  hhcnf  31841  eleigvec  31893  isst  32149  ishst  32150  cvnbtwn3  32224  cvnbtwn4  32225  chirredi  32330  sumdmdii  32351  an42ds  32386  an52ds  32387  an62ds  32388  an72ds  32389  an82ds  32390  or3di  32395  rexunirn  32428  rmoun  32430  dmrab  32433  difrab2  32434  iunin1f  32493  disjunsn  32530  opeldifid  32535  ofpreima  32596  mpomptxf  32608  fdifsupp  32615  1stpreima  32637  2ndpreima  32638  f1od2  32651  resf1o  32660  maprnin  32661  nndiffz1  32716  ismnt  32916  mgcval  32920  omndmul2  33033  erler  33223  isorng  33284  opprnsg  33462  1arithidom  33515  1arithufdlem4  33525  smatrcl  33793  ordtconnlem1  33921  isrrext  33997  sigaex  34107  sigaval  34108  omssubaddlem  34297  omssubadd  34298  eulerpartleme  34361  eulerpartlemt0  34367  eulerpartlemr  34372  eulerpartlemn  34379  probun  34417  ballotlemelo  34486  ballotlem2  34487  ballotlemfc0  34491  ballotlemfcc  34492  reprdifc  34625  bnj248  34697  bnj250  34698  bnj268  34706  bnj312  34709  bnj945  34770  bnj110  34855  bnj849  34922  bnj882  34923  bnj893  34925  bnj916  34930  bnj983  34948  bnj1040  34969  bnj1175  35001  cusgredgex  35116  cusgr3cyclex  35130  erdszelem1  35185  iscvm  35253  elmpst  35530  mpstrcl  35535  dfso3  35714  xpab  35720  coepr  35747  dfdm5  35767  dfrn5  35768  elima4  35770  fv1stcnv  35771  fv2ndcnv  35772  brpprod  35880  dfon3  35887  elfix  35898  dffix2  35900  elfuns  35910  brimg  35932  brapply  35933  brsuccf  35936  funpartlem  35937  funpartfun  35938  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  lineunray  36142  ellines  36147  rmoeqi  36182  reueqi  36184  itgeq12i  36201  finminlem  36313  fneval  36347  neibastop3  36357  eliminable-abelv  36864  bj-inrab  36922  bj-rest10  37083  bj-restpw  37087  bj-restuni  37092  bj-mpomptALT  37114  bj-imdirco  37185  icorempo  37346  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlpssretop  37359  pibt2  37412  wl-ifp-ncond2  37460  wl-df3-3mintru2  37481  wl-2mintru1  37485  rabiun  37594  iundif1  37595  lindsenlbs  37616  poimirlem4  37625  poimirlem25  37646  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnclem2  37673  itg2addnclem3  37674  itg2addnc  37675  ftc1anc  37702  isbnd2  37784  bndss  37787  heibor1lem  37810  heibor1  37811  isrngohom  37966  isidl  38015  sbccom2lem  38125  anan  38224  eqbrb  38228  eqelb  38230  br1cnvinxp  38252  eldmqsres  38282  idinxpssinxp2  38313  moantr  38353  inxpxrn  38388  dfcoss3  38412  cocossss  38434  ressn2  38440  br1cossinidres  38447  br1cossincnvepres  38448  br1cossxrnidres  38449  br1cossxrncnvepres  38450  refrelcoss2  38462  symrelcoss2  38464  cosscnvssid5  38476  br1cossxrncnvssrres  38506  dfrefrel3  38514  dfcnvrefrel3  38529  cosselcnvrefrels2  38536  cosselcnvrefrels3  38537  cosselcnvrefrels4  38538  cosselcnvrefrels5  38539  dfsymrel3  38548  refsymrel2  38565  refsymrel3  38566  elrefsymrels3  38568  dftrrel3  38576  dfeqvrel2  38588  dfeqvrel3  38589  redundpbi1  38629  refrelredund3  38635  eldmqs1cossres  38658  dffunALTV2  38687  dffunALTV3  38688  dffunALTV4  38689  dffunALTV5  38690  dfdisjALTV  38712  dfdisjALTV2  38713  dfdisjALTV3  38714  dfdisjALTV4  38715  eldisjs3  38723  eldisjs4  38724  disjsuc  38758  prtlem70  38857  prtlem100  38859  prter2  38881  lsateln0  38995  islshpat  39017  lcvnbtwn3  39028  islfl  39060  ishlat1  39352  ishlat2  39353  cvrat4  39444  islvol5  39580  psubspset  39745  snatpsubN  39751  dalawlem13  39884  psubclsetN  39937  isltrn2N  40121  cdlemftr3  40566  dibelval3  41148  dicval2  41180  dicopelval2  41182  dicelval2N  41183  dihglb2  41343  islpolN  41484  lcfls1c  41537  mapdvalc  41630  mapdval4N  41633  mapdordlem1a  41635  aks4d1p8  42082  fimgmcyc  42529  prjsperref  42601  prjspeclsp  42607  elmzpcl  42721  mzpindd  42741  fphpd  42811  pw2f1ocnv  43033  islmodfg  43065  islssfg2  43067  dflim6  43260  onsucf1olem  43266  omge2  43294  tfsconcatlem  43332  tfsconcat0i  43341  rp-isfinite6  43514  minregex  43530  elmapintrab  43572  elinintrab  43573  relintab  43579  dfrtrcl5  43625  fsovrfovd  44005  ntrk1k3eqk13  44046  gneispace3  44129  k0004lem1  44143  pm13.192  44406  opelopab4  44548  ax6e2nd  44555  en3lplem2VD  44840  ax6e2ndVD  44904  ax6e2ndALT  44926  permaxrep  45003  iuneq1i  45086  ssrabf  45115  limcrecl  45634  dvnprodlem2  45952  fourierdlem103  46214  fourierdlem104  46215  4an21  47275  sprvalpwn0  47488  pairreueq  47515  dfvopnbgr2  47857  isubgredg  47870  xpsnopab  48149  sgrp2sgrp  48220  mpomptx2  48327  lindslinindsimp1  48450  lindslinindsimp2  48456  itsclc0b  48765  mo0sn  48808  coxp  48825  isthincd2  49430  thinccic  49464  2arwcatlem1  49588  setc1onsubc  49595  alsconv  49783  aacllem  49794