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  2472  rexcomf  3268  cbvreu  3386  rabeqi  3408  rabrabi  3414  rabrab  3419  ceqsex3v  3492  spc2ed  3556  rexrab  3656  reurab  3661  rmo3f  3694  reuind  3713  rmo3  3841  ssrab  4024  rexun  4147  elin3  4157  inass  4179  rexin  4201  dfun2  4221  inrab2  4268  rabun2  4275  reuun2  4276  undif4  4418  rexdifpr  4611  rexsns  4623  rexdifsn  4745  2ralunsn  4846  iuncom4  4950  iindif1  5024  iunxiun  5046  disjxun  5090  zfrep4  5232  inuni  5289  reusv2lem4  5340  reusv2  5342  otth2  5426  copsexgw  5433  copsexg  5434  copsex2g  5436  copsex4g  5438  vopelopabsb  5472  rabxp  5667  opeliunxp  5686  opeliun2xp  5687  xpundir  5689  xpiundi  5690  xpiundir  5691  brinxp2  5697  copsex2gb  5749  cnvopab  6086  dminss  6102  imainss  6103  difxp  6113  cnvresima  6179  coundi  6196  resco  6199  imaco  6200  rnco  6201  coiun  6205  coi1  6211  coass  6214  cnvpo  6235  xpco  6237  dfpo2  6244  frpoind  6290  dffun2  6492  fncnv  6555  imadif  6566  mptun  6628  ffrnb  6666  dff1o2  6769  dff1o3  6770  brprcneu  6812  brprcneuALT  6813  fvun2  6915  eqfnfv3  6967  respreima  7000  f1ompt  7045  f1ossf1o  7062  fsn  7069  fmptsng  7104  fmptsnd  7105  tpres  7137  abrexco  7180  imaiun  7181  f1mpt  7198  dff1o6  7212  imaeqsexvOLD  7300  riotarab  7348  oprabidw  7380  oprabid  7381  dfoprab2  7407  oprab4  7435  mpomptx  7462  elpwpwel  7703  elxp4  7855  elxp5  7856  ffoss  7881  f11o  7882  opabex3d  7900  opabex3rd  7901  opabex3  7902  abexssex  7905  elxp7  7959  dfopab2  7987  dfoprab3s  7988  fsplit  8050  frxp  8059  xporderlem  8060  frpoins3xp3g  8074  soseq  8092  suppssov1  8130  suppssov2  8131  suppssfv  8135  brtpos2  8165  tpostpos  8179  tposmpo  8196  dfrecs3  8295  oarec  8480  oeeu  8521  eldifsucnn  8582  naddasslem1  8612  mapsncnv  8820  dfixp  8826  domen  8887  xpsnen  8978  xpcomco  8984  xpassen  8988  sbthlem9  9012  frfi  9174  marypha2lem2  9326  brttrcl2  9610  epfrs  9627  tcsni  9639  frind  9646  cp  9787  dfac5lem1  10017  dfac5lem2  10018  dfac5lem5  10021  kmlem3  10047  dfackm  10061  cfval2  10154  cflim3  10156  cfss  10159  cfslb  10160  zfcndrep  10508  eltsk2g  10645  ltexpi  10796  recmulnq  10858  ltexprlem4  10933  addsrpr  10969  mulsrpr  10970  addcnsr  11029  mulcnsr  11030  ltresr  11034  axrrecex  11057  elnnz  12481  elnn0z  12484  fnn0ind  12575  rexuz2  12800  rexrp  12916  elixx3g  13261  elfz2  13417  elfzuzb  13421  fznn  13495  elfz2nn0  13521  fznn0  13522  4fvwrd4  13551  preduz  13553  elfzo2  13565  fzind2  13688  hashgt23el  14331  hashf1lem1  14362  hashf1lem2  14363  fz1isolem  14368  s4f1o  14825  wwlktovfo  14865  fsum2dlem  15677  modfsummod  15701  prodeq1i  15823  sinltx  16098  divalglem10  16313  divalgb  16315  coprmproddvdslem  16573  isprm2  16593  infpn2  16825  prdsle  17366  prdsless  17367  prdsleval  17381  imasleval  17445  xpscf  17469  dfiso2  17679  oppcsect  17685  elhoma  17939  ispos2  18221  lubeldm  18257  glbeldm  18270  tosso  18323  ismgmhm  18570  issubmgm  18576  submgmacs  18591  ismhm  18659  issubm  18677  submacs  18701  issubg  19005  issubg3  19023  gaorb  19186  pmtrrn2  19339  efgcpbllema  19633  efgcpbllemb  19634  frgpuplem  19651  imasabl  19755  subgdmdprd  19915  dprd2d2  19925  omndmul2  20012  dfrhm2  20359  opprnzrb  20406  issubrg  20456  isdomn3  20600  drngprop  20629  drngid2  20637  opprdrng  20649  isabv  20696  isorng  20746  islss  20837  islbs  20980  lsmspsn  20988  isobs  21627  islinds  21716  isassa  21763  aspval2  21805  ltbval  21948  opsrle  21952  opsrtoslem1  21960  fvmptnn04if  22734  ntreq0  22962  restntr  23067  cnnei  23167  hausnei2  23238  cmpcov2  23275  cmpsub  23285  uncmp  23288  cmpfi  23293  llyi  23359  dissnlocfin  23414  iskgen3  23434  1stckgenlem  23438  ptpjpre1  23456  txcnpi  23493  txtube  23525  hausdiag  23530  txlm  23533  txkgen  23537  cfinfil  23778  csdfil  23779  supfil  23780  fin1aufil  23817  elflim2  23849  hauspwpwf1  23872  txflf  23891  isfcls  23894  alexsubALTlem3  23934  alexsubALT  23936  cnextcn  23952  istmd  23959  istgp  23962  tgphaus  24002  qustgplem  24006  istrg  24049  istdrg  24051  istlm  24070  blres  24317  isms2  24336  metrest  24410  metuel2  24451  restmetu  24456  isngp  24482  isnlm  24561  elii1  24829  isclmp  24995  iscvsp  25026  isncvsngp  25047  iscph  25068  cfilucfil3  25218  isbn  25236  limcrcl  25773  ig1pval3  26081  plydivex  26203  ellogdm  26546  cubic  26757  dmarea  26865  vmasum  27125  lgsquadlem1  27289  lgsquadlem2  27290  elno3  27565  slenlt  27662  madeval2  27763  elnnzs  28294  istrkg3ld  28406  legov  28530  ltgov  28542  colinearalg  28855  axeuclid  28908  axcontlem2  28910  axcontlem5  28913  nbgrel  29285  nbupgrres  29309  nbusgredgeu0  29313  nb3grprlem2  29326  nb3grpr2  29328  nb3gr2nb  29329  cplgr3v  29380  finsumvtxdg2ssteplem3  29493  wlkonprop  29602  upgrtrls  29645  upgristrl  29646  wksonproplem  29648  usgr2pth0  29710  wwlksnext  29838  wwlksnextsurj  29845  wwlksnfi  29851  wspthsnwspthsnon  29861  wpthswwlks2on  29906  rusgrnumwwlkl1  29913  erclwwlkref  29964  isclwwlknx  29980  clwwlknwwlksn  29982  clwwlkel  29990  erclwwlknref  30013  clwlknf1oclwwlkn  30028  clwwlknonel  30039  clwwlknon1  30041  clwwlknon2x  30047  clwwlkvbij  30057  iseupthf1o  30146  2pthfrgrrn  30226  fusgr2wsp2nb  30278  numclwwlk1lem2f1  30301  numclwwlkovh  30317  numclwlk2lem2f1o  30323  frgrregord013  30339  avril1  30407  islno  30697  h2hlm  30924  hcau  31128  hhsssh2  31214  dfch2  31351  elcnop  31801  ellnop  31802  elhmop  31817  elcnfn  31826  ellnfn  31827  dmadjss  31831  adjeu  31833  adjval  31834  hhcno  31848  hhcnf  31849  eleigvec  31901  isst  32157  ishst  32158  cvnbtwn3  32232  cvnbtwn4  32233  chirredi  32338  sumdmdii  32359  an42ds  32394  an52ds  32395  an62ds  32396  an72ds  32397  an82ds  32398  or3di  32403  rexunirn  32436  rmoun  32438  dmrab  32441  difrab2  32442  iunin1f  32501  disjunsn  32538  opeldifid  32543  ofpreima  32608  mpomptxf  32620  fdifsupp  32627  1stpreima  32649  2ndpreima  32650  f1od2  32663  resf1o  32673  maprnin  32674  nndiffz1  32729  ismnt  32925  mgcval  32929  erler  33205  opprnsg  33421  1arithidom  33474  1arithufdlem4  33484  extdgfialglem1  33659  smatrcl  33763  ordtconnlem1  33891  isrrext  33967  sigaex  34077  sigaval  34078  omssubaddlem  34267  omssubadd  34268  eulerpartleme  34331  eulerpartlemt0  34337  eulerpartlemr  34342  eulerpartlemn  34349  probun  34387  ballotlemelo  34456  ballotlem2  34457  ballotlemfc0  34461  ballotlemfcc  34462  reprdifc  34595  bnj248  34667  bnj250  34668  bnj268  34676  bnj312  34679  bnj945  34740  bnj110  34825  bnj849  34892  bnj882  34893  bnj893  34895  bnj916  34900  bnj983  34918  bnj1040  34939  bnj1175  34971  cusgredgex  35095  cusgr3cyclex  35109  erdszelem1  35164  iscvm  35232  elmpst  35509  mpstrcl  35514  dfso3  35693  xpab  35699  coepr  35726  dfdm5  35746  dfrn5  35747  elima4  35749  fv1stcnv  35750  fv2ndcnv  35751  brpprod  35859  dfon3  35866  elfix  35877  dffix2  35879  elfuns  35889  brimg  35911  brapply  35912  brsuccf  35915  funpartlem  35916  funpartfun  35917  brrestrict  35923  dfrecs2  35924  dfrdg4  35925  lineunray  36121  ellines  36126  rmoeqi  36161  reueqi  36163  itgeq12i  36180  finminlem  36292  fneval  36326  neibastop3  36336  eliminable-abelv  36843  bj-inrab  36901  bj-rest10  37062  bj-restpw  37066  bj-restuni  37071  bj-mpomptALT  37093  bj-imdirco  37164  icorempo  37325  isbasisrelowllem1  37329  isbasisrelowllem2  37330  relowlpssretop  37338  pibt2  37391  wl-ifp-ncond2  37439  wl-df3-3mintru2  37460  wl-2mintru1  37464  rabiun  37573  iundif1  37574  lindsenlbs  37595  poimirlem4  37604  poimirlem25  37625  poimirlem26  37626  poimirlem29  37629  poimirlem30  37630  ismblfin  37641  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  itg2addnclem2  37652  itg2addnclem3  37653  itg2addnc  37654  ftc1anc  37681  isbnd2  37763  bndss  37766  heibor1lem  37789  heibor1  37790  isrngohom  37945  isidl  37994  sbccom2lem  38104  anan  38203  eqbrb  38207  eqelb  38209  br1cnvinxp  38231  eldmqsres  38261  idinxpssinxp2  38292  moantr  38332  inxpxrn  38367  dfcoss3  38391  cocossss  38413  ressn2  38419  br1cossinidres  38426  br1cossincnvepres  38427  br1cossxrnidres  38428  br1cossxrncnvepres  38429  refrelcoss2  38441  symrelcoss2  38443  cosscnvssid5  38455  br1cossxrncnvssrres  38485  dfrefrel3  38493  dfcnvrefrel3  38508  cosselcnvrefrels2  38515  cosselcnvrefrels3  38516  cosselcnvrefrels4  38517  cosselcnvrefrels5  38518  dfsymrel3  38527  refsymrel2  38544  refsymrel3  38545  elrefsymrels3  38547  dftrrel3  38555  dfeqvrel2  38567  dfeqvrel3  38568  redundpbi1  38608  refrelredund3  38614  eldmqs1cossres  38637  dffunALTV2  38666  dffunALTV3  38667  dffunALTV4  38668  dffunALTV5  38669  dfdisjALTV  38691  dfdisjALTV2  38692  dfdisjALTV3  38693  dfdisjALTV4  38694  eldisjs3  38702  eldisjs4  38703  disjsuc  38737  prtlem70  38836  prtlem100  38838  prter2  38860  lsateln0  38974  islshpat  38996  lcvnbtwn3  39007  islfl  39039  ishlat1  39331  ishlat2  39332  cvrat4  39422  islvol5  39558  psubspset  39723  snatpsubN  39729  dalawlem13  39862  psubclsetN  39915  isltrn2N  40099  cdlemftr3  40544  dibelval3  41126  dicval2  41158  dicopelval2  41160  dicelval2N  41161  dihglb2  41321  islpolN  41462  lcfls1c  41515  mapdvalc  41608  mapdval4N  41611  mapdordlem1a  41613  aks4d1p8  42060  fimgmcyc  42507  prjsperref  42579  prjspeclsp  42585  elmzpcl  42699  mzpindd  42719  fphpd  42789  pw2f1ocnv  43010  islmodfg  43042  islssfg2  43044  dflim6  43237  onsucf1olem  43243  omge2  43271  tfsconcatlem  43309  tfsconcat0i  43318  rp-isfinite6  43491  minregex  43507  elmapintrab  43549  elinintrab  43550  relintab  43556  dfrtrcl5  43602  fsovrfovd  43982  ntrk1k3eqk13  44023  gneispace3  44106  k0004lem1  44120  pm13.192  44383  opelopab4  44525  ax6e2nd  44532  en3lplem2VD  44817  ax6e2ndVD  44881  ax6e2ndALT  44903  permaxrep  44980  iuneq1i  45063  ssrabf  45092  limcrecl  45610  dvnprodlem2  45928  fourierdlem103  46190  fourierdlem104  46191  4an21  47254  sprvalpwn0  47467  pairreueq  47494  dfvopnbgr2  47837  isubgredg  47850  xpsnopab  48141  sgrp2sgrp  48212  mpomptx2  48319  lindslinindsimp1  48442  lindslinindsimp2  48448  itsclc0b  48757  mo0sn  48800  coxp  48817  isthincd2  49422  thinccic  49456  2arwcatlem1  49580  setc1onsubc  49587  alsconv  49775  aacllem  49786