Theorem anbi1i 630

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 580	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi2ci  631  bianbi  633  anandi  682  3an4anass  1110  3ioran  1111  4anpull2  1368  an33rean  1491  an42ds  1497  19.26-3an  1879  sb3an  2092  eeeanv  2358  sbel2x  2482  rexcomf  3278  cbvreu  3383  rabeqi  3404  rabrabi  3410  rabrab  3415  ceqsex3v  3484  spc2ed  3539  rexrab  3637  reurab  3642  rmo3f  3675  reuind  3694  rmo3  3821  ssrab  4002  rexun  4125  elin3  4135  inass  4156  rexin  4178  dfun2  4198  inrab2  4245  rabun2  4252  reuun2  4253  undif4  4395  rexdifpr  4591  rexsns  4603  rexdifsn  4727  2ralunsn  4826  iuncom4  4930  iindif1  5004  iunxiun  5026  disjxun  5070  zfrep4  5215  inuni  5278  reusv2lem4  5330  reusv2  5332  otth2  5423  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  copsex2g  5434  copsex4g  5436  vopelopabsb  5471  rabxp  5666  opeliunxp  5685  opeliun2xp  5686  xpundir  5688  xpiundi  5689  xpiundir  5690  brinxp2  5696  copsex2gb  5749  cnvopab  6087  dminss  6104  imainss  6105  difxp  6115  cnvresima  6181  coundi  6198  resco  6201  imaco  6202  rnco  6203  rncoOLD  6204  coiun  6208  coi1  6214  coass  6217  cnvpo  6238  xpco  6240  dfpo2  6247  frpoind  6293  dffun2  6495  fncnv  6558  imadif  6569  mptun  6631  ffrnb  6669  dff1o2  6772  dff1o3  6773  brprcneu  6817  brprcneuALT  6818  fvun2  6919  eqfnfv3  6973  respreima  7007  f1ompt  7052  f1ossf1o  7070  fsn  7077  fmptsng  7112  fmptsnd  7113  tpres  7145  abrexco  7188  imaiun  7189  f1mpt  7205  dff1o6  7219  imaeqsexvOLD  7307  riotarab  7355  oprabidw  7387  oprabid  7388  dfoprab2  7414  oprab4  7442  mpomptx  7469  elpwpwel  7710  elxp4  7862  elxp5  7863  ffoss  7888  f11o  7889  opabex3d  7907  opabex3rd  7908  opabex3  7909  abexssex  7912  elxp7  7966  dfopab2  7994  dfoprab3s  7995  fsplit  8056  frxp  8066  xporderlem  8067  frpoins3xp3g  8081  soseq  8099  suppssov1  8137  suppssov2  8138  suppssfv  8142  brtpos2  8172  tpostpos  8186  tposmpo  8203  dfrecs3  8302  oarec  8487  oeeu  8529  eldifsucnn  8590  naddasslem1  8620  mapsncnv  8831  dfixp  8837  domen  8898  xpsnen  8989  xpcomco  8995  xpassen  8999  sbthlem9  9023  frfi  9185  marypha2lem2  9339  brttrcl2  9626  epfrs  9643  tcsni  9653  frind  9665  cp  9806  dfac5lem1  10036  dfac5lem2  10037  dfac5lem5  10040  kmlem3  10066  dfackm  10080  cfval2  10173  cflim3  10175  cfss  10178  cfslb  10179  zfcndrep  10528  eltsk2g  10665  ltexpi  10816  recmulnq  10878  ltexprlem4  10953  addsrpr  10989  mulsrpr  10990  addcnsr  11049  mulcnsr  11050  ltresr  11054  axrrecex  11077  elnnz  12525  elnn0z  12528  fnn0ind  12619  rexuz2  12840  rexrp  12956  elixx3g  13302  elfz2  13459  elfzuzb  13463  fznn  13537  elfz2nn0  13563  fznn0  13564  4fvwrd4  13593  preduz  13595  elfzo2  13607  fzind2  13734  hashgt23el  14377  hashf1lem1  14408  hashf1lem2  14409  fz1isolem  14414  s4f1o  14871  wwlktovfo  14911  fsum2dlem  15723  modfsummod  15748  prodeq1i  15872  sinltx  16147  divalglem10  16362  divalgb  16364  coprmproddvdslem  16622  isprm2  16642  infpn2  16875  prdsle  17416  prdsless  17417  prdsleval  17431  imasleval  17496  xpscf  17520  dfiso2  17730  oppcsect  17736  elhoma  17990  ispos2  18272  lubeldm  18308  glbeldm  18321  tosso  18374  ismgmhm  18655  issubmgm  18661  submgmacs  18676  ismhm  18744  issubm  18762  submacs  18786  issubg  19093  issubg3  19111  gaorb  19273  pmtrrn2  19426  efgcpbllema  19720  efgcpbllemb  19721  frgpuplem  19738  imasabl  19842  subgdmdprd  20002  dprd2d2  20012  omndmul2  20099  dfrhm2  20445  opprnzrb  20493  issubrg  20543  isdomn3  20687  drngprop  20716  drngid2  20724  opprdrng  20736  isabv  20783  isorng  20833  islss  20924  islbs  21066  lsmspsn  21074  isobs  21695  islinds  21784  isassa  21831  aspval2  21873  ltbval  22019  opsrle  22023  opsrtoslem1  22031  fvmptnn04if  22832  ntreq0  23060  restntr  23165  cnnei  23265  hausnei2  23336  cmpcov2  23373  cmpsub  23383  uncmp  23386  cmpfi  23391  llyi  23457  dissnlocfin  23512  iskgen3  23532  1stckgenlem  23536  ptpjpre1  23554  txcnpi  23591  txtube  23623  hausdiag  23628  txlm  23631  txkgen  23635  cfinfil  23876  csdfil  23877  supfil  23878  fin1aufil  23915  elflim2  23947  hauspwpwf1  23970  txflf  23989  isfcls  23992  alexsubALTlem3  24032  alexsubALT  24034  cnextcn  24050  istmd  24057  istgp  24060  tgphaus  24100  qustgplem  24104  istrg  24147  istdrg  24149  istlm  24168  blres  24414  isms2  24433  metrest  24507  metuel2  24548  restmetu  24553  isngp  24579  isnlm  24658  elii1  24920  isclmp  25082  iscvsp  25113  isncvsngp  25134  iscph  25155  cfilucfil3  25305  isbn  25323  limcrcl  25859  ig1pval3  26161  plydivex  26281  ellogdm  26621  cubic  26831  dmarea  26939  vmasum  27197  lgsquadlem1  27361  lgsquadlem2  27362  elno3  27637  lenlts  27734  madeval2  27843  elnnzs  28411  istrkg3ld  28547  legov  28671  ltgov  28683  colinearalg  28997  axeuclid  29050  axcontlem2  29052  axcontlem5  29055  nbgrel  29427  nbupgrres  29451  nbusgredgeu0  29455  nb3grprlem2  29468  nb3grpr2  29470  nb3gr2nb  29471  cplgr3v  29522  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  32646  disjunsn  32683  opeldifid  32688  ofpreima  32757  mpomptxf  32770  fdifsupp  32777  1stpreima  32799  2ndpreima  32800  f1od2  32811  resf1o  32822  maprnin  32823  nndiffz1  32878  ismnt  33062  mgcval  33066  erler  33346  opprnsg  33567  1arithidom  33620  1arithufdlem4  33630  extdgfialglem1  33876  smatrcl  33980  ordtconnlem1  34108  isrrext  34184  sigaex  34294  sigaval  34295  omssubaddlem  34483  omssubadd  34484  eulerpartleme  34547  eulerpartlemt0  34553  eulerpartlemr  34558  eulerpartlemn  34565  probun  34603  ballotlemelo  34672  ballotlem2  34673  ballotlemfc0  34677  ballotlemfcc  34678  reprdifc  34811  bnj248  34883  bnj250  34884  bnj268  34892  bnj312  34895  bnj945  34956  bnj110  35040  bnj849  35107  bnj882  35108  bnj893  35110  bnj916  35115  bnj983  35133  bnj1040  35154  bnj1175  35186  cusgredgex  35350  cusgr3cyclex  35364  erdszelem1  35419  iscvm  35487  elmpst  35764  mpstrcl  35769  dfso3  35948  xpab  35954  coepr  35981  dfdm5  36001  dfrn5  36002  elima4  36004  fv1stcnv  36005  fv2ndcnv  36006  brpprod  36111  dfon3  36118  elfix  36129  dffix2  36131  elfuns  36141  brimg  36163  brapply  36164  lemsuccf  36167  funpartlem  36170  funpartfun  36171  brrestrict  36177  dfrecs2  36178  dfrdg4  36179  lineunray  36375  ellines  36380  rmoeqi  36415  reueqi  36417  itgeq12i  36434  finminlem  36546  fneval  36580  neibastop3  36590  eliminable-abelv  37222  bj-inrab  37280  bj-axseprep  37427  bj-rest10  37446  bj-restpw  37450  bj-restuni  37455  bj-mpomptALT  37477  copsex2gd  37498  bj-imdirco  37550  icorempo  37713  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlpssretop  37726  pibt2  37779  wl-ifp-ncond2  37827  wl-df3-3mintru2  37848  wl-2mintru1  37852  rabiun  37960  iundif1  37961  lindsenlbs  37982  poimirlem4  37991  poimirlem25  38012  poimirlem26  38013  poimirlem29  38016  poimirlem30  38017  ismblfin  38028  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  ftc1anc  38068  isbnd2  38150  bndss  38153  heibor1lem  38176  heibor1  38177  isrngohom  38332  isidl  38381  sbccom2lem  38491  anan  38602  eqbrb  38606  eqelb  38608  br1cnvinxp  38626  eldmqsres  38660  idinxpssinxp2  38691  moantr  38739  inxpxrn  38785  blockadjliftmap  38825  dfcoss3  38871  cocossss  38893  ressn2  38899  br1cossinidres  38906  br1cossincnvepres  38907  br1cossxrnidres  38908  br1cossxrncnvepres  38909  refrelcoss2  38921  symrelcoss2  38923  cosscnvssid5  38935  br1cossxrncnvssrres  38955  dfrefrel3  38963  dfcnvrefrel3  38978  cosselcnvrefrels2  38985  cosselcnvrefrels3  38986  cosselcnvrefrels4  38987  cosselcnvrefrels5  38988  dfsymrel3  39001  refsymrel2  39018  refsymrel3  39019  elrefsymrels3  39021  dftrrel3  39029  dfeqvrel2  39041  dfeqvrel3  39042  redundpbi1  39082  refrelredund3  39088  eldmqs1cossres  39111  dffunALTV2  39140  dffunALTV3  39141  dffunALTV4  39142  dffunALTV5  39143  dfdisjALTV  39165  dfdisjALTV2  39166  dfdisjALTV3  39167  dfdisjALTV4  39168  disjimdmqseq  39176  eldisjs3  39188  eldisjs4  39189  disjsuc  39226  prtlem70  39349  prtlem100  39351  prter2  39373  lsateln0  39487  islshpat  39509  lcvnbtwn3  39520  islfl  39552  ishlat1  39844  ishlat2  39845  cvrat4  39935  islvol5  40071  psubspset  40236  snatpsubN  40242  dalawlem13  40375  psubclsetN  40428  isltrn2N  40612  cdlemftr3  41057  dibelval3  41639  dicval2  41671  dicopelval2  41673  dicelval2N  41674  dihglb2  41834  islpolN  41975  lcfls1c  42028  mapdvalc  42121  mapdval4N  42124  mapdordlem1a  42126  aks4d1p8  42572  fimgmcyc  43020  prjsperref  43056  prjspeclsp  43062  elmzpcl  43175  mzpindd  43195  fphpd  43261  pw2f1ocnv  43482  islmodfg  43514  islssfg2  43516  dflim6  43709  onsucf1olem  43715  omge2  43743  tfsconcatlem  43781  tfsconcat0i  43790  rp-isfinite6  43962  minregex  43978  elmapintrab  44020  elinintrab  44021  relintab  44027  dfrtrcl5  44073  fsovrfovd  44453  ntrk1k3eqk13  44494  gneispace3  44577  k0004lem1  44591  pm13.192  44854  opelopab4  44995  ax6e2nd  45002  en3lplem2VD  45287  ax6e2ndVD  45351  ax6e2ndALT  45373  permaxrep  45450  iuneq1i  45532  ssrabf  45561  limcrecl  46074  dvnprodlem2  46390  fourierdlem103  46652  fourierdlem104  46653  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