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  an42ds  1491  19.26-3an  1873  sb3an  2086  eeeanv  2352  sbel2x  2476  rexcomf  3273  cbvreu  3389  rabeqi  3410  rabrabi  3416  rabrab  3421  ceqsex3v  3493  spc2ed  3553  rexrab  3652  reurab  3657  rmo3f  3690  reuind  3709  rmo3  3837  ssrab  4021  rexun  4146  elin3  4156  inass  4178  rexin  4200  dfun2  4220  inrab2  4267  rabun2  4274  reuun2  4275  undif4  4417  rexdifpr  4614  rexsns  4626  rexdifsn  4748  2ralunsn  4849  iuncom4  4953  iindif1  5028  iunxiun  5050  disjxun  5094  zfrep4  5236  inuni  5293  reusv2lem4  5344  reusv2  5346  otth2  5429  copsexgw  5436  copsexg  5437  copsex2g  5439  copsex4g  5441  vopelopabsb  5475  rabxp  5670  opeliunxp  5689  opeliun2xp  5690  xpundir  5692  xpiundi  5693  xpiundir  5694  brinxp2  5700  copsex2gb  5753  cnvopab  6092  dminss  6109  imainss  6110  difxp  6120  cnvresima  6186  coundi  6203  resco  6206  imaco  6207  rnco  6208  rncoOLD  6209  coiun  6213  coi1  6219  coass  6222  cnvpo  6243  xpco  6245  dfpo2  6252  frpoind  6298  dffun2  6500  fncnv  6563  imadif  6574  mptun  6636  ffrnb  6674  dff1o2  6777  dff1o3  6778  brprcneu  6822  brprcneuALT  6823  fvun2  6924  eqfnfv3  6976  respreima  7009  f1ompt  7054  f1ossf1o  7071  fsn  7078  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  8057  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  8829  dfixp  8835  domen  8896  xpsnen  8987  xpcomco  8993  xpassen  8997  sbthlem9  9021  frfi  9183  marypha2lem2  9337  brttrcl2  9621  epfrs  9638  tcsni  9648  frind  9660  cp  9801  dfac5lem1  10031  dfac5lem2  10032  dfac5lem5  10035  kmlem3  10061  dfackm  10075  cfval2  10168  cflim3  10170  cfss  10173  cfslb  10174  zfcndrep  10523  eltsk2g  10660  ltexpi  10811  recmulnq  10873  ltexprlem4  10948  addsrpr  10984  mulsrpr  10985  addcnsr  11044  mulcnsr  11045  ltresr  11049  axrrecex  11072  elnnz  12496  elnn0z  12499  fnn0ind  12589  rexuz2  12810  rexrp  12926  elixx3g  13272  elfz2  13428  elfzuzb  13432  fznn  13506  elfz2nn0  13532  fznn0  13533  4fvwrd4  13562  preduz  13564  elfzo2  13576  fzind2  13702  hashgt23el  14345  hashf1lem1  14376  hashf1lem2  14377  fz1isolem  14382  s4f1o  14839  wwlktovfo  14879  fsum2dlem  15691  modfsummod  15715  prodeq1i  15837  sinltx  16112  divalglem10  16327  divalgb  16329  coprmproddvdslem  16587  isprm2  16607  infpn2  16839  prdsle  17380  prdsless  17381  prdsleval  17395  imasleval  17460  xpscf  17484  dfiso2  17694  oppcsect  17700  elhoma  17954  ispos2  18236  lubeldm  18272  glbeldm  18285  tosso  18338  ismgmhm  18619  issubmgm  18625  submgmacs  18640  ismhm  18708  issubm  18726  submacs  18750  issubg  19054  issubg3  19072  gaorb  19234  pmtrrn2  19387  efgcpbllema  19681  efgcpbllemb  19682  frgpuplem  19699  imasabl  19803  subgdmdprd  19963  dprd2d2  19973  omndmul2  20060  dfrhm2  20408  opprnzrb  20452  issubrg  20502  isdomn3  20646  drngprop  20675  drngid2  20683  opprdrng  20695  isabv  20742  isorng  20792  islss  20883  islbs  21026  lsmspsn  21034  isobs  21673  islinds  21762  isassa  21809  aspval2  21852  ltbval  21996  opsrle  22000  opsrtoslem1  22008  fvmptnn04if  22791  ntreq0  23019  restntr  23124  cnnei  23224  hausnei2  23295  cmpcov2  23332  cmpsub  23342  uncmp  23345  cmpfi  23350  llyi  23416  dissnlocfin  23471  iskgen3  23491  1stckgenlem  23495  ptpjpre1  23513  txcnpi  23550  txtube  23582  hausdiag  23587  txlm  23590  txkgen  23594  cfinfil  23835  csdfil  23836  supfil  23837  fin1aufil  23874  elflim2  23906  hauspwpwf1  23929  txflf  23948  isfcls  23951  alexsubALTlem3  23991  alexsubALT  23993  cnextcn  24009  istmd  24016  istgp  24019  tgphaus  24059  qustgplem  24063  istrg  24106  istdrg  24108  istlm  24127  blres  24373  isms2  24392  metrest  24466  metuel2  24507  restmetu  24512  isngp  24538  isnlm  24617  elii1  24885  isclmp  25051  iscvsp  25082  isncvsngp  25103  iscph  25124  cfilucfil3  25274  isbn  25292  limcrcl  25829  ig1pval3  26137  plydivex  26259  ellogdm  26602  cubic  26813  dmarea  26921  vmasum  27181  lgsquadlem1  27345  lgsquadlem2  27346  elno3  27621  slenlt  27718  madeval2  27821  elnnzs  28359  istrkg3ld  28482  legov  28606  ltgov  28618  colinearalg  28932  axeuclid  28985  axcontlem2  28987  axcontlem5  28990  nbgrel  29362  nbupgrres  29386  nbusgredgeu0  29390  nb3grprlem2  29403  nb3grpr2  29405  nb3gr2nb  29406  cplgr3v  29457  finsumvtxdg2ssteplem3  29570  wlkonprop  29679  upgrtrls  29722  upgristrl  29723  wksonproplem  29725  usgr2pth0  29787  wwlksnext  29915  wwlksnextsurj  29922  wwlksnfi  29928  wspthsnwspthsnon  29938  wpthswwlks2on  29986  rusgrnumwwlkl1  29993  erclwwlkref  30044  isclwwlknx  30060  clwwlknwwlksn  30062  clwwlkel  30070  erclwwlknref  30093  clwlknf1oclwwlkn  30108  clwwlknonel  30119  clwwlknon1  30121  clwwlknon2x  30127  clwwlkvbij  30137  iseupthf1o  30226  2pthfrgrrn  30306  fusgr2wsp2nb  30358  numclwwlk1lem2f1  30381  numclwwlkovh  30397  numclwlk2lem2f1o  30403  frgrregord013  30419  avril1  30487  islno  30777  h2hlm  31004  hcau  31208  hhsssh2  31294  dfch2  31431  elcnop  31881  ellnop  31882  elhmop  31897  elcnfn  31906  ellnfn  31907  dmadjss  31911  adjeu  31913  adjval  31914  hhcno  31928  hhcnf  31929  eleigvec  31981  isst  32237  ishst  32238  cvnbtwn3  32312  cvnbtwn4  32313  chirredi  32418  sumdmdii  32439  an52ds  32474  an62ds  32475  an72ds  32476  an82ds  32477  or3di  32482  rexunirn  32515  rmoun  32517  dmrab  32520  difrab2  32521  iunin1f  32581  disjunsn  32618  opeldifid  32623  ofpreima  32692  mpomptxf  32706  fdifsupp  32713  1stpreima  32735  2ndpreima  32736  f1od2  32747  resf1o  32758  maprnin  32759  nndiffz1  32815  ismnt  33014  mgcval  33018  erler  33296  opprnsg  33514  1arithidom  33567  1arithufdlem4  33577  extdgfialglem1  33798  smatrcl  33902  ordtconnlem1  34030  isrrext  34106  sigaex  34216  sigaval  34217  omssubaddlem  34405  omssubadd  34406  eulerpartleme  34469  eulerpartlemt0  34475  eulerpartlemr  34480  eulerpartlemn  34487  probun  34525  ballotlemelo  34594  ballotlem2  34595  ballotlemfc0  34599  ballotlemfcc  34600  reprdifc  34733  bnj248  34805  bnj250  34806  bnj268  34814  bnj312  34817  bnj945  34878  bnj110  34963  bnj849  35030  bnj882  35031  bnj893  35033  bnj916  35038  bnj983  35056  bnj1040  35077  bnj1175  35109  cusgredgex  35265  cusgr3cyclex  35279  erdszelem1  35334  iscvm  35402  elmpst  35679  mpstrcl  35684  dfso3  35863  xpab  35869  coepr  35896  dfdm5  35916  dfrn5  35917  elima4  35919  fv1stcnv  35920  fv2ndcnv  35921  brpprod  36026  dfon3  36033  elfix  36044  dffix2  36046  elfuns  36056  brimg  36078  brapply  36079  lemsuccf  36082  funpartlem  36085  funpartfun  36086  brrestrict  36092  dfrecs2  36093  dfrdg4  36094  lineunray  36290  ellines  36295  rmoeqi  36330  reueqi  36332  itgeq12i  36349  finminlem  36461  fneval  36495  neibastop3  36505  eliminable-abelv  37013  bj-inrab  37071  bj-rest10  37232  bj-restpw  37236  bj-restuni  37241  bj-mpomptALT  37263  bj-imdirco  37334  icorempo  37495  isbasisrelowllem1  37499  isbasisrelowllem2  37500  relowlpssretop  37508  pibt2  37561  wl-ifp-ncond2  37609  wl-df3-3mintru2  37630  wl-2mintru1  37634  rabiun  37733  iundif1  37734  lindsenlbs  37755  poimirlem4  37764  poimirlem25  37785  poimirlem26  37786  poimirlem29  37789  poimirlem30  37790  ismblfin  37801  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  itg2addnclem2  37812  itg2addnclem3  37813  itg2addnc  37814  ftc1anc  37841  isbnd2  37923  bndss  37926  heibor1lem  37949  heibor1  37950  isrngohom  38105  isidl  38154  sbccom2lem  38264  anan  38370  eqbrb  38374  eqelb  38376  br1cnvinxp  38393  eldmqsres  38425  idinxpssinxp2  38456  moantr  38496  inxpxrn  38542  blockadjliftmap  38572  dfcoss3  38616  cocossss  38638  ressn2  38644  br1cossinidres  38651  br1cossincnvepres  38652  br1cossxrnidres  38653  br1cossxrncnvepres  38654  refrelcoss2  38666  symrelcoss2  38668  cosscnvssid5  38680  br1cossxrncnvssrres  38700  dfrefrel3  38708  dfcnvrefrel3  38723  cosselcnvrefrels2  38730  cosselcnvrefrels3  38731  cosselcnvrefrels4  38732  cosselcnvrefrels5  38733  dfsymrel3  38746  refsymrel2  38763  refsymrel3  38764  elrefsymrels3  38766  dftrrel3  38774  dfeqvrel2  38786  dfeqvrel3  38787  redundpbi1  38827  refrelredund3  38833  eldmqs1cossres  38857  dffunALTV2  38886  dffunALTV3  38887  dffunALTV4  38888  dffunALTV5  38889  dfdisjALTV  38911  dfdisjALTV2  38912  dfdisjALTV3  38913  dfdisjALTV4  38914  eldisjs3  38922  eldisjs4  38923  disjsuc  38957  prtlem70  39056  prtlem100  39058  prter2  39080  lsateln0  39194  islshpat  39216  lcvnbtwn3  39227  islfl  39259  ishlat1  39551  ishlat2  39552  cvrat4  39642  islvol5  39778  psubspset  39943  snatpsubN  39949  dalawlem13  40082  psubclsetN  40135  isltrn2N  40319  cdlemftr3  40764  dibelval3  41346  dicval2  41378  dicopelval2  41380  dicelval2N  41381  dihglb2  41541  islpolN  41682  lcfls1c  41735  mapdvalc  41828  mapdval4N  41831  mapdordlem1a  41833  aks4d1p8  42280  fimgmcyc  42731  prjsperref  42791  prjspeclsp  42797  elmzpcl  42910  mzpindd  42930  fphpd  43000  pw2f1ocnv  43221  islmodfg  43253  islssfg2  43255  dflim6  43448  onsucf1olem  43454  omge2  43482  tfsconcatlem  43520  tfsconcat0i  43529  rp-isfinite6  43701  minregex  43717  elmapintrab  43759  elinintrab  43760  relintab  43766  dfrtrcl5  43812  fsovrfovd  44192  ntrk1k3eqk13  44233  gneispace3  44316  k0004lem1  44330  pm13.192  44593  opelopab4  44734  ax6e2nd  44741  en3lplem2VD  45026  ax6e2ndVD  45090  ax6e2ndALT  45112  permaxrep  45189  iuneq1i  45271  ssrabf  45300  limcrecl  45817  dvnprodlem2  46133  fourierdlem103  46395  fourierdlem104  46396  4an21  47458  sprvalpwn0  47671  pairreueq  47698  dfvopnbgr2  48041  isubgredg  48054  xpsnopab  48345  sgrp2sgrp  48416  mpomptx2  48523  lindslinindsimp1  48645  lindslinindsimp2  48651  itsclc0b  48960  mo0sn  49003  coxp  49020  isthincd2  49624  thinccic  49658  2arwcatlem1  49782  setc1onsubc  49789  alsconv  49977  aacllem  49988