Theorem anbi1i 623

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  624  bianbi  626  anandi  675  3an4anass  1105  3ioran  1106  an6  1445  an33rean  1483  19.26-3an  1871  sb3an  2081  eeeanv  2356  sbel2x  2482  rexcomf  3309  cbvreuwOLD  3423  cbvreu  3435  rabeqi  3457  rabrabi  3463  rabrab  3468  ceqsex3v  3549  spc2ed  3614  rexabOLD  3717  rexrab  3718  reurab  3723  rmo3f  3756  reuind  3775  rmo3  3911  ssrab  4096  rexun  4219  elin3  4229  inass  4249  rexin  4269  dfun2  4289  inrab2  4336  rabun2  4343  reuun2  4344  undif4  4490  rexdifpr  4681  rexsns  4693  rexdifsn  4819  2ralunsn  4919  iuncom4  5023  iindif1  5098  iunxiun  5120  disjxun  5164  zfrep4  5314  inuni  5368  reusv2lem4  5419  reusv2  5421  otth2  5503  copsexgw  5510  copsexg  5511  copsex2g  5513  copsex4g  5514  vopelopabsb  5548  rabxp  5748  opeliunxp  5767  xpundir  5769  xpiundi  5770  xpiundir  5771  brinxp2  5777  copsex2gb  5830  cnvopab  6169  dminss  6184  imainss  6185  difxp  6195  cnvresima  6261  coundi  6278  resco  6281  imaco  6282  rnco  6283  coiun  6287  coi1  6293  coass  6296  cnvpo  6318  xpco  6320  dfpo2  6327  frpoind  6374  wfiOLD  6383  dffun2  6583  dffun2OLD  6584  dffun2OLDOLD  6585  fncnv  6651  imadif  6662  mptun  6726  ffrnb  6761  dff1o2  6867  dff1o3  6868  brprcneu  6910  brprcneuALT  6911  fvun2  7014  eqfnfv3  7066  respreima  7099  f1ompt  7145  f1ossf1o  7162  fsn  7169  fmptsng  7202  fmptsnd  7203  tpres  7238  abrexco  7281  imaiun  7282  f1mpt  7298  dff1o6  7311  imaeqsexvOLD  7399  riotarab  7447  oprabidw  7479  oprabid  7480  dfoprab2  7508  oprab4  7536  mpomptx  7563  elpwpwel  7802  elxp4  7962  elxp5  7963  ffoss  7986  f11o  7987  opabex3d  8006  opabex3rd  8007  opabex3  8008  abexssex  8011  elxp7  8065  dfopab2  8093  dfoprab3s  8094  fsplit  8158  frxp  8167  xporderlem  8168  frpoins3xp3g  8182  soseq  8200  suppssov1  8238  suppssov2  8239  suppssfv  8243  brtpos2  8273  tpostpos  8287  tposmpo  8304  wfrfunOLD  8375  dfrecs3  8428  dfrecs3OLD  8429  oarec  8618  oeeu  8659  eldifsucnn  8720  naddasslem1  8750  mapsncnv  8951  dfixp  8957  domen  9021  xpsnen  9121  xpcomco  9128  xpassen  9132  sbthlem9  9157  frfi  9349  marypha2lem2  9505  brttrcl2  9783  epfrs  9800  tcsni  9812  frind  9819  cp  9960  dfac5lem1  10192  dfac5lem2  10193  dfac5lem5  10196  kmlem3  10222  dfackm  10236  cfval2  10329  cflim3  10331  cfss  10334  cfslb  10335  zfcndrep  10683  eltsk2g  10820  ltexpi  10971  recmulnq  11033  ltexprlem4  11108  addsrpr  11144  mulsrpr  11145  addcnsr  11204  mulcnsr  11205  ltresr  11209  axrrecex  11232  elnnz  12649  elnn0z  12652  fnn0ind  12742  rexuz2  12964  rexrp  13078  elixx3g  13420  elfz2  13574  elfzuzb  13578  fznn  13652  elfz2nn0  13675  fznn0  13676  4fvwrd4  13705  preduz  13707  elfzo2  13719  fzind2  13835  hashgt23el  14473  hashf1lem1  14504  hashf1lem2  14505  fz1isolem  14510  s4f1o  14967  wwlktovfo  15007  fsum2dlem  15818  modfsummod  15842  prodeq1i  15964  sinltx  16237  divalglem10  16450  divalgb  16452  coprmproddvdslem  16709  isprm2  16729  infpn2  16960  prdsle  17522  prdsless  17523  prdsleval  17537  imasleval  17601  xpscf  17625  dfiso2  17833  oppcsect  17839  elhoma  18099  ispos2  18385  lubeldm  18423  glbeldm  18436  tosso  18489  ismgmhm  18734  issubmgm  18740  submgmacs  18755  ismhm  18820  issubm  18838  submacs  18862  issubg  19166  issubg3  19184  gaorb  19347  pmtrrn2  19502  efgcpbllema  19796  efgcpbllemb  19797  frgpuplem  19814  imasabl  19918  subgdmdprd  20078  dprd2d2  20088  dfrhm2  20500  opprnzrb  20547  issubrg  20599  isdomn3  20737  drngprop  20766  drngid2  20774  opprdrng  20786  isabv  20834  islss  20955  islbs  21098  lsmspsn  21106  isobs  21763  islinds  21852  isassa  21899  aspval2  21941  ltbval  22084  opsrle  22088  opsrtoslem1  22102  fvmptnn04if  22876  ntreq0  23106  restntr  23211  cnnei  23311  hausnei2  23382  cmpcov2  23419  cmpsub  23429  uncmp  23432  cmpfi  23437  llyi  23503  dissnlocfin  23558  iskgen3  23578  1stckgenlem  23582  ptpjpre1  23600  txcnpi  23637  txtube  23669  hausdiag  23674  txlm  23677  txkgen  23681  cfinfil  23922  csdfil  23923  supfil  23924  fin1aufil  23961  elflim2  23993  hauspwpwf1  24016  txflf  24035  isfcls  24038  alexsubALTlem3  24078  alexsubALT  24080  cnextcn  24096  istmd  24103  istgp  24106  tgphaus  24146  qustgplem  24150  istrg  24193  istdrg  24195  istlm  24214  blres  24462  isms2  24481  metrest  24558  metuel2  24599  restmetu  24604  isngp  24630  isnlm  24717  elii1  24983  isclmp  25149  iscvsp  25180  isncvsngp  25202  iscph  25223  cfilucfil3  25373  isbn  25391  limcrcl  25929  ig1pval3  26237  plydivex  26357  ellogdm  26699  cubic  26910  dmarea  27018  vmasum  27278  lgsquadlem1  27442  lgsquadlem2  27443  elno3  27718  slenlt  27815  madeval2  27910  elnnzs  28405  istrkg3ld  28487  legov  28611  ltgov  28623  colinearalg  28943  axeuclid  28996  axcontlem2  28998  axcontlem5  29001  nbgrel  29375  nbupgrres  29399  nbusgredgeu0  29403  nb3grprlem2  29416  nb3grpr2  29418  nb3gr2nb  29419  cplgr3v  29470  finsumvtxdg2ssteplem3  29583  wlkonprop  29694  upgrtrls  29737  upgristrl  29738  wksonproplem  29740  wksonproplemOLD  29741  usgr2pth0  29801  wwlksnext  29926  wwlksnextsurj  29933  wwlksnfi  29939  wspthsnwspthsnon  29949  wpthswwlks2on  29994  rusgrnumwwlkl1  30001  erclwwlkref  30052  isclwwlknx  30068  clwwlknwwlksn  30070  clwwlkel  30078  erclwwlknref  30101  clwlknf1oclwwlkn  30116  clwwlknonel  30127  clwwlknon1  30129  clwwlknon2x  30135  clwwlkvbij  30145  iseupthf1o  30234  2pthfrgrrn  30314  fusgr2wsp2nb  30366  numclwwlk1lem2f1  30389  numclwwlkovh  30405  numclwlk2lem2f1o  30411  frgrregord013  30427  avril1  30495  islno  30785  h2hlm  31012  hcau  31216  hhsssh2  31302  dfch2  31439  elcnop  31889  ellnop  31890  elhmop  31905  elcnfn  31914  ellnfn  31915  dmadjss  31919  adjeu  31921  adjval  31922  hhcno  31936  hhcnf  31937  eleigvec  31989  isst  32245  ishst  32246  cvnbtwn3  32320  cvnbtwn4  32321  chirredi  32426  sumdmdii  32447  an42ds  32479  an52ds  32480  an62ds  32481  an72ds  32482  an82ds  32483  or3di  32488  rexunirn  32520  rmoun  32522  dmrab  32525  difrab2  32526  iunin1f  32580  disjunsn  32616  opeldifid  32621  ofpreima  32683  mpomptxf  32695  1stpreima  32718  2ndpreima  32719  f1od2  32735  resf1o  32744  maprnin  32745  nndiffz1  32791  ismnt  32956  mgcval  32960  omndmul2  33062  erler  33237  isorng  33294  opprnsg  33477  1arithidom  33530  1arithufdlem4  33540  smatrcl  33742  ordtconnlem1  33870  isrrext  33946  sigaex  34074  sigaval  34075  omssubaddlem  34264  omssubadd  34265  eulerpartleme  34328  eulerpartlemt0  34334  eulerpartlemr  34339  eulerpartlemn  34346  probun  34384  ballotlemelo  34452  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  reprdifc  34604  bnj248  34676  bnj250  34677  bnj268  34685  bnj312  34688  bnj945  34749  bnj110  34834  bnj849  34901  bnj882  34902  bnj893  34904  bnj916  34909  bnj983  34927  bnj1040  34948  bnj1175  34980  cusgredgex  35089  cusgr3cyclex  35104  erdszelem1  35159  iscvm  35227  elmpst  35504  mpstrcl  35509  dfso3  35682  xpab  35688  coepr  35715  dfdm5  35736  dfrn5  35737  elima4  35739  fv1stcnv  35740  fv2ndcnv  35741  brpprod  35849  dfon3  35856  elfix  35867  dffix2  35869  elfuns  35879  brimg  35901  brapply  35902  brsuccf  35905  funpartlem  35906  funpartfun  35907  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  lineunray  36111  ellines  36116  rmoeqi  36151  reueqi  36153  itgeq12i  36170  finminlem  36284  fneval  36318  neibastop3  36328  eliminable-abelv  36835  bj-inrab  36893  bj-rest10  37054  bj-restpw  37058  bj-restuni  37063  bj-mpomptALT  37085  bj-imdirco  37156  icorempo  37317  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlpssretop  37330  pibt2  37383  wl-ifp-ncond2  37431  wl-df3-3mintru2  37452  wl-2mintru1  37456  rabiun  37553  iundif1  37554  lindsenlbs  37575  poimirlem4  37584  poimirlem25  37605  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem2  37632  itg2addnclem3  37633  itg2addnc  37634  ftc1anc  37661  isbnd2  37743  bndss  37746  heibor1lem  37769  heibor1  37770  isrngohom  37925  isidl  37974  sbccom2lem  38084  anan  38183  eqbrb  38188  eqelb  38190  br1cnvinxp  38212  eldmqsres  38243  idinxpssinxp2  38274  moantr  38320  inxpxrn  38351  dfcoss3  38370  cocossss  38392  ressn2  38398  br1cossinidres  38405  br1cossincnvepres  38406  br1cossxrnidres  38407  br1cossxrncnvepres  38408  refrelcoss2  38420  symrelcoss2  38422  cosscnvssid5  38434  br1cossxrncnvssrres  38464  dfrefrel3  38472  dfcnvrefrel3  38487  cosselcnvrefrels2  38494  cosselcnvrefrels3  38495  cosselcnvrefrels4  38496  cosselcnvrefrels5  38497  dfsymrel3  38506  refsymrel2  38523  refsymrel3  38524  elrefsymrels3  38526  dftrrel3  38534  dfeqvrel2  38546  dfeqvrel3  38547  redundpbi1  38587  refrelredund3  38593  eldmqs1cossres  38615  dffunALTV2  38644  dffunALTV3  38645  dffunALTV4  38646  dffunALTV5  38647  dfdisjALTV  38669  dfdisjALTV2  38670  dfdisjALTV3  38671  dfdisjALTV4  38672  eldisjs3  38680  eldisjs4  38681  disjsuc  38715  prtlem70  38813  prtlem100  38815  prter2  38837  lsateln0  38951  islshpat  38973  lcvnbtwn3  38984  islfl  39016  ishlat1  39308  ishlat2  39309  cvrat4  39400  islvol5  39536  psubspset  39701  snatpsubN  39707  dalawlem13  39840  psubclsetN  39893  isltrn2N  40077  cdlemftr3  40522  dibelval3  41104  dicval2  41136  dicopelval2  41138  dicelval2N  41139  dihglb2  41299  islpolN  41440  lcfls1c  41493  mapdvalc  41586  mapdval4N  41589  mapdordlem1a  41591  aks4d1p8  42044  fimgmcyc  42489  prjsperref  42561  prjspeclsp  42567  elmzpcl  42682  mzpindd  42702  fphpd  42772  pw2f1ocnv  42994  islmodfg  43026  islssfg2  43028  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  44379  opelopab4  44522  ax6e2nd  44529  en3lplem2VD  44815  ax6e2ndVD  44879  ax6e2ndALT  44901  iuneq1i  44987  ssrabf  45016  limcrecl  45550  dvnprodlem2  45868  fourierdlem103  46130  fourierdlem104  46131  4an21  47185  sprvalpwn0  47357  pairreueq  47384  dfvopnbgr2  47725  xpsnopab  47880  sgrp2sgrp  47951  opeliun2xp  48057  mpomptx2  48059  lindslinindsimp1  48186  lindslinindsimp2  48192  itsclc0b  48506  mo0sn  48547  iscnrm3lem3  48615  isthincd2  48705  thinccic  48728  alsconv  48884  aacllem  48895