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  3275  cbvreu  3394  rabeqi  3416  rabrabi  3422  rabrab  3427  ceqsex3v  3500  spc2ed  3564  rexrab  3664  reurab  3669  rmo3f  3702  reuind  3721  rmo3  3849  ssrab  4032  rexun  4155  elin3  4165  inass  4187  rexin  4209  dfun2  4229  inrab2  4276  rabun2  4283  reuun2  4284  undif4  4426  rexdifpr  4619  rexsns  4631  rexdifsn  4754  2ralunsn  4855  iuncom4  4960  iindif1  5034  iunxiun  5056  disjxun  5100  zfrep4  5243  inuni  5300  reusv2lem4  5351  reusv2  5353  otth2  5438  copsexgw  5445  copsexg  5446  copsex2g  5448  copsex4g  5450  vopelopabsb  5484  rabxp  5679  opeliunxp  5698  opeliun2xp  5699  xpundir  5701  xpiundi  5702  xpiundir  5703  brinxp2  5709  copsex2gb  5760  cnvopab  6098  dminss  6114  imainss  6115  difxp  6125  cnvresima  6191  coundi  6208  resco  6211  imaco  6212  rnco  6213  coiun  6217  coi1  6223  coass  6226  cnvpo  6248  xpco  6250  dfpo2  6257  frpoind  6303  dffun2  6509  dffun2OLD  6510  fncnv  6573  imadif  6584  mptun  6646  ffrnb  6684  dff1o2  6787  dff1o3  6788  brprcneu  6830  brprcneuALT  6831  fvun2  6935  eqfnfv3  6987  respreima  7020  f1ompt  7065  f1ossf1o  7082  fsn  7089  fmptsng  7124  fmptsnd  7125  tpres  7157  abrexco  7200  imaiun  7201  f1mpt  7218  dff1o6  7232  imaeqsexvOLD  7320  riotarab  7368  oprabidw  7400  oprabid  7401  dfoprab2  7427  oprab4  7455  mpomptx  7482  elpwpwel  7723  elxp4  7878  elxp5  7879  ffoss  7904  f11o  7905  opabex3d  7923  opabex3rd  7924  opabex3  7925  abexssex  7928  elxp7  7982  dfopab2  8010  dfoprab3s  8011  fsplit  8073  frxp  8082  xporderlem  8083  frpoins3xp3g  8097  soseq  8115  suppssov1  8153  suppssov2  8154  suppssfv  8158  brtpos2  8188  tpostpos  8202  tposmpo  8219  dfrecs3  8318  oarec  8503  oeeu  8544  eldifsucnn  8605  naddasslem1  8635  mapsncnv  8843  dfixp  8849  domen  8910  xpsnen  9002  xpcomco  9008  xpassen  9012  sbthlem9  9036  frfi  9208  marypha2lem2  9363  brttrcl2  9643  epfrs  9660  tcsni  9672  frind  9679  cp  9820  dfac5lem1  10052  dfac5lem2  10053  dfac5lem5  10056  kmlem3  10082  dfackm  10096  cfval2  10189  cflim3  10191  cfss  10194  cfslb  10195  zfcndrep  10543  eltsk2g  10680  ltexpi  10831  recmulnq  10893  ltexprlem4  10968  addsrpr  11004  mulsrpr  11005  addcnsr  11064  mulcnsr  11065  ltresr  11069  axrrecex  11092  elnnz  12515  elnn0z  12518  fnn0ind  12609  rexuz2  12834  rexrp  12950  elixx3g  13295  elfz2  13451  elfzuzb  13455  fznn  13529  elfz2nn0  13555  fznn0  13556  4fvwrd4  13585  preduz  13587  elfzo2  13599  fzind2  13722  hashgt23el  14365  hashf1lem1  14396  hashf1lem2  14397  fz1isolem  14402  s4f1o  14860  wwlktovfo  14900  fsum2dlem  15712  modfsummod  15736  prodeq1i  15858  sinltx  16133  divalglem10  16348  divalgb  16350  coprmproddvdslem  16608  isprm2  16628  infpn2  16860  prdsle  17401  prdsless  17402  prdsleval  17416  imasleval  17480  xpscf  17504  dfiso2  17710  oppcsect  17716  elhoma  17970  ispos2  18252  lubeldm  18288  glbeldm  18301  tosso  18354  ismgmhm  18599  issubmgm  18605  submgmacs  18620  ismhm  18688  issubm  18706  submacs  18730  issubg  19034  issubg3  19052  gaorb  19215  pmtrrn2  19366  efgcpbllema  19660  efgcpbllemb  19661  frgpuplem  19678  imasabl  19782  subgdmdprd  19942  dprd2d2  19952  dfrhm2  20359  opprnzrb  20406  issubrg  20456  isdomn3  20600  drngprop  20629  drngid2  20637  opprdrng  20649  isabv  20696  islss  20816  islbs  20959  lsmspsn  20967  isobs  21605  islinds  21694  isassa  21741  aspval2  21783  ltbval  21926  opsrle  21930  opsrtoslem1  21938  fvmptnn04if  22712  ntreq0  22940  restntr  23045  cnnei  23145  hausnei2  23216  cmpcov2  23253  cmpsub  23263  uncmp  23266  cmpfi  23271  llyi  23337  dissnlocfin  23392  iskgen3  23412  1stckgenlem  23416  ptpjpre1  23434  txcnpi  23471  txtube  23503  hausdiag  23508  txlm  23511  txkgen  23515  cfinfil  23756  csdfil  23757  supfil  23758  fin1aufil  23795  elflim2  23827  hauspwpwf1  23850  txflf  23869  isfcls  23872  alexsubALTlem3  23912  alexsubALT  23914  cnextcn  23930  istmd  23937  istgp  23940  tgphaus  23980  qustgplem  23984  istrg  24027  istdrg  24029  istlm  24048  blres  24295  isms2  24314  metrest  24388  metuel2  24429  restmetu  24434  isngp  24460  isnlm  24539  elii1  24807  isclmp  24973  iscvsp  25004  isncvsngp  25025  iscph  25046  cfilucfil3  25196  isbn  25214  limcrcl  25751  ig1pval3  26059  plydivex  26181  ellogdm  26524  cubic  26735  dmarea  26843  vmasum  27103  lgsquadlem1  27267  lgsquadlem2  27268  elno3  27543  slenlt  27640  madeval2  27737  elnnzs  28265  istrkg3ld  28364  legov  28488  ltgov  28500  colinearalg  28813  axeuclid  28866  axcontlem2  28868  axcontlem5  28871  nbgrel  29243  nbupgrres  29267  nbusgredgeu0  29271  nb3grprlem2  29284  nb3grpr2  29286  nb3gr2nb  29287  cplgr3v  29338  finsumvtxdg2ssteplem3  29451  wlkonprop  29560  upgrtrls  29603  upgristrl  29604  wksonproplem  29606  usgr2pth0  29668  wwlksnext  29796  wwlksnextsurj  29803  wwlksnfi  29809  wspthsnwspthsnon  29819  wpthswwlks2on  29864  rusgrnumwwlkl1  29871  erclwwlkref  29922  isclwwlknx  29938  clwwlknwwlksn  29940  clwwlkel  29948  erclwwlknref  29971  clwlknf1oclwwlkn  29986  clwwlknonel  29997  clwwlknon1  29999  clwwlknon2x  30005  clwwlkvbij  30015  iseupthf1o  30104  2pthfrgrrn  30184  fusgr2wsp2nb  30236  numclwwlk1lem2f1  30259  numclwwlkovh  30275  numclwlk2lem2f1o  30281  frgrregord013  30297  avril1  30365  islno  30655  h2hlm  30882  hcau  31086  hhsssh2  31172  dfch2  31309  elcnop  31759  ellnop  31760  elhmop  31775  elcnfn  31784  ellnfn  31785  dmadjss  31789  adjeu  31791  adjval  31792  hhcno  31806  hhcnf  31807  eleigvec  31859  isst  32115  ishst  32116  cvnbtwn3  32190  cvnbtwn4  32191  chirredi  32296  sumdmdii  32317  an42ds  32352  an52ds  32353  an62ds  32354  an72ds  32355  an82ds  32356  or3di  32361  rexunirn  32394  rmoun  32396  dmrab  32399  difrab2  32400  iunin1f  32459  disjunsn  32496  opeldifid  32501  ofpreima  32562  mpomptxf  32574  fdifsupp  32581  1stpreima  32603  2ndpreima  32604  f1od2  32617  resf1o  32626  maprnin  32627  nndiffz1  32682  ismnt  32882  mgcval  32886  omndmul2  32999  erler  33189  isorng  33250  opprnsg  33428  1arithidom  33481  1arithufdlem4  33491  smatrcl  33759  ordtconnlem1  33887  isrrext  33963  sigaex  34073  sigaval  34074  omssubaddlem  34263  omssubadd  34264  eulerpartleme  34327  eulerpartlemt0  34333  eulerpartlemr  34338  eulerpartlemn  34345  probun  34383  ballotlemelo  34452  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  reprdifc  34591  bnj248  34663  bnj250  34664  bnj268  34672  bnj312  34675  bnj945  34736  bnj110  34821  bnj849  34888  bnj882  34889  bnj893  34891  bnj916  34896  bnj983  34914  bnj1040  34935  bnj1175  34967  cusgredgex  35082  cusgr3cyclex  35096  erdszelem1  35151  iscvm  35219  elmpst  35496  mpstrcl  35501  dfso3  35680  xpab  35686  coepr  35713  dfdm5  35733  dfrn5  35734  elima4  35736  fv1stcnv  35737  fv2ndcnv  35738  brpprod  35846  dfon3  35853  elfix  35864  dffix2  35866  elfuns  35876  brimg  35898  brapply  35899  brsuccf  35902  funpartlem  35903  funpartfun  35904  brrestrict  35910  dfrecs2  35911  dfrdg4  35912  lineunray  36108  ellines  36113  rmoeqi  36148  reueqi  36150  itgeq12i  36167  finminlem  36279  fneval  36313  neibastop3  36323  eliminable-abelv  36830  bj-inrab  36888  bj-rest10  37049  bj-restpw  37053  bj-restuni  37058  bj-mpomptALT  37080  bj-imdirco  37151  icorempo  37312  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlpssretop  37325  pibt2  37378  wl-ifp-ncond2  37426  wl-df3-3mintru2  37447  wl-2mintru1  37451  rabiun  37560  iundif1  37561  lindsenlbs  37582  poimirlem4  37591  poimirlem25  37612  poimirlem26  37613  poimirlem29  37616  poimirlem30  37617  ismblfin  37628  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  itg2addnclem2  37639  itg2addnclem3  37640  itg2addnc  37641  ftc1anc  37668  isbnd2  37750  bndss  37753  heibor1lem  37776  heibor1  37777  isrngohom  37932  isidl  37981  sbccom2lem  38091  anan  38190  eqbrb  38194  eqelb  38196  br1cnvinxp  38218  eldmqsres  38248  idinxpssinxp2  38279  moantr  38319  inxpxrn  38354  dfcoss3  38378  cocossss  38400  ressn2  38406  br1cossinidres  38413  br1cossincnvepres  38414  br1cossxrnidres  38415  br1cossxrncnvepres  38416  refrelcoss2  38428  symrelcoss2  38430  cosscnvssid5  38442  br1cossxrncnvssrres  38472  dfrefrel3  38480  dfcnvrefrel3  38495  cosselcnvrefrels2  38502  cosselcnvrefrels3  38503  cosselcnvrefrels4  38504  cosselcnvrefrels5  38505  dfsymrel3  38514  refsymrel2  38531  refsymrel3  38532  elrefsymrels3  38534  dftrrel3  38542  dfeqvrel2  38554  dfeqvrel3  38555  redundpbi1  38595  refrelredund3  38601  eldmqs1cossres  38624  dffunALTV2  38653  dffunALTV3  38654  dffunALTV4  38655  dffunALTV5  38656  dfdisjALTV  38678  dfdisjALTV2  38679  dfdisjALTV3  38680  dfdisjALTV4  38681  eldisjs3  38689  eldisjs4  38690  disjsuc  38724  prtlem70  38823  prtlem100  38825  prter2  38847  lsateln0  38961  islshpat  38983  lcvnbtwn3  38994  islfl  39026  ishlat1  39318  ishlat2  39319  cvrat4  39410  islvol5  39546  psubspset  39711  snatpsubN  39717  dalawlem13  39850  psubclsetN  39903  isltrn2N  40087  cdlemftr3  40532  dibelval3  41114  dicval2  41146  dicopelval2  41148  dicelval2N  41149  dihglb2  41309  islpolN  41450  lcfls1c  41503  mapdvalc  41596  mapdval4N  41599  mapdordlem1a  41601  aks4d1p8  42048  fimgmcyc  42495  prjsperref  42567  prjspeclsp  42573  elmzpcl  42687  mzpindd  42707  fphpd  42777  pw2f1ocnv  42999  islmodfg  43031  islssfg2  43033  dflim6  43226  onsucf1olem  43232  omge2  43260  tfsconcatlem  43298  tfsconcat0i  43307  rp-isfinite6  43480  minregex  43496  elmapintrab  43538  elinintrab  43539  relintab  43545  dfrtrcl5  43591  fsovrfovd  43971  ntrk1k3eqk13  44012  gneispace3  44095  k0004lem1  44109  pm13.192  44372  opelopab4  44514  ax6e2nd  44521  en3lplem2VD  44806  ax6e2ndVD  44870  ax6e2ndALT  44892  permaxrep  44969  iuneq1i  45052  ssrabf  45081  limcrecl  45600  dvnprodlem2  45918  fourierdlem103  46180  fourierdlem104  46181  4an21  47244  sprvalpwn0  47457  pairreueq  47484  dfvopnbgr2  47826  isubgredg  47839  xpsnopab  48118  sgrp2sgrp  48189  mpomptx2  48296  lindslinindsimp1  48419  lindslinindsimp2  48425  itsclc0b  48734  mo0sn  48777  coxp  48794  isthincd2  49399  thinccic  49433  2arwcatlem1  49557  setc1onsubc  49564  alsconv  49752  aacllem  49763