Theorem anbi1i 625

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  626  bianbi  628  anandi  677  3an4anass  1105  3ioran  1106  4anpull2  1363  an33rean  1486  an42ds  1492  19.26-3an  1874  sb3an  2087  eeeanv  2355  sbel2x  2479  rexcomf  3277  cbvreu  3382  rabeqi  3403  rabrabi  3409  rabrab  3414  ceqsex3v  3484  spc2ed  3544  rexrab  3643  reurab  3648  rmo3f  3681  reuind  3700  rmo3  3828  ssrab  4012  rexun  4137  elin3  4147  inass  4169  rexin  4191  dfun2  4211  inrab2  4258  rabun2  4265  reuun2  4266  undif4  4408  rexdifpr  4604  rexsns  4616  rexdifsn  4738  2ralunsn  4839  iuncom4  4943  iindif1  5018  iunxiun  5040  disjxun  5084  zfrep4  5228  inuni  5285  reusv2lem4  5336  reusv2  5338  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  6977  respreima  7010  f1ompt  7055  f1ossf1o  7073  fsn  7080  fmptsng  7114  fmptsnd  7115  tpres  7147  abrexco  7190  imaiun  7191  f1mpt  7207  dff1o6  7221  imaeqsexvOLD  7309  riotarab  7357  oprabidw  7389  oprabid  7390  dfoprab2  7416  oprab4  7444  mpomptx  7471  elpwpwel  7712  elxp4  7864  elxp5  7865  ffoss  7890  f11o  7891  opabex3d  7909  opabex3rd  7910  opabex3  7911  abexssex  7914  elxp7  7968  dfopab2  7996  dfoprab3s  7997  fsplit  8058  frxp  8067  xporderlem  8068  frpoins3xp3g  8082  soseq  8100  suppssov1  8138  suppssov2  8139  suppssfv  8143  brtpos2  8173  tpostpos  8187  tposmpo  8204  dfrecs3  8303  oarec  8488  oeeu  8530  eldifsucnn  8591  naddasslem1  8621  mapsncnv  8832  dfixp  8838  domen  8899  xpsnen  8990  xpcomco  8996  xpassen  9000  sbthlem9  9024  frfi  9186  marypha2lem2  9340  brttrcl2  9624  epfrs  9641  tcsni  9651  frind  9663  cp  9804  dfac5lem1  10034  dfac5lem2  10035  dfac5lem5  10038  kmlem3  10064  dfackm  10078  cfval2  10171  cflim3  10173  cfss  10176  cfslb  10177  zfcndrep  10526  eltsk2g  10663  ltexpi  10814  recmulnq  10876  ltexprlem4  10951  addsrpr  10987  mulsrpr  10988  addcnsr  11047  mulcnsr  11048  ltresr  11052  axrrecex  11075  elnnz  12499  elnn0z  12502  fnn0ind  12592  rexuz2  12813  rexrp  12929  elixx3g  13275  elfz2  13431  elfzuzb  13435  fznn  13509  elfz2nn0  13535  fznn0  13536  4fvwrd4  13565  preduz  13567  elfzo2  13579  fzind2  13705  hashgt23el  14348  hashf1lem1  14379  hashf1lem2  14380  fz1isolem  14385  s4f1o  14842  wwlktovfo  14882  fsum2dlem  15694  modfsummod  15718  prodeq1i  15840  sinltx  16115  divalglem10  16330  divalgb  16332  coprmproddvdslem  16590  isprm2  16610  infpn2  16842  prdsle  17383  prdsless  17384  prdsleval  17398  imasleval  17463  xpscf  17487  dfiso2  17697  oppcsect  17703  elhoma  17957  ispos2  18239  lubeldm  18275  glbeldm  18288  tosso  18341  ismgmhm  18622  issubmgm  18628  submgmacs  18643  ismhm  18711  issubm  18729  submacs  18753  issubg  19060  issubg3  19078  gaorb  19240  pmtrrn2  19393  efgcpbllema  19687  efgcpbllemb  19688  frgpuplem  19705  imasabl  19809  subgdmdprd  19969  dprd2d2  19979  omndmul2  20066  dfrhm2  20412  opprnzrb  20456  issubrg  20506  isdomn3  20650  drngprop  20679  drngid2  20687  opprdrng  20699  isabv  20746  isorng  20796  islss  20887  islbs  21030  lsmspsn  21038  isobs  21677  islinds  21766  isassa  21813  aspval2  21855  ltbval  21999  opsrle  22003  opsrtoslem1  22011  fvmptnn04if  22792  ntreq0  23020  restntr  23125  cnnei  23225  hausnei2  23296  cmpcov2  23333  cmpsub  23343  uncmp  23346  cmpfi  23351  llyi  23417  dissnlocfin  23472  iskgen3  23492  1stckgenlem  23496  ptpjpre1  23514  txcnpi  23551  txtube  23583  hausdiag  23588  txlm  23591  txkgen  23595  cfinfil  23836  csdfil  23837  supfil  23838  fin1aufil  23875  elflim2  23907  hauspwpwf1  23930  txflf  23949  isfcls  23952  alexsubALTlem3  23992  alexsubALT  23994  cnextcn  24010  istmd  24017  istgp  24020  tgphaus  24060  qustgplem  24064  istrg  24107  istdrg  24109  istlm  24128  blres  24374  isms2  24393  metrest  24467  metuel2  24508  restmetu  24513  isngp  24539  isnlm  24618  elii1  24880  isclmp  25042  iscvsp  25073  isncvsngp  25094  iscph  25115  cfilucfil3  25265  isbn  25283  limcrcl  25819  ig1pval3  26124  plydivex  26245  ellogdm  26588  cubic  26799  dmarea  26907  vmasum  27167  lgsquadlem1  27331  lgsquadlem2  27332  elno3  27607  lenlts  27704  madeval2  27813  elnnzs  28381  istrkg3ld  28517  legov  28641  ltgov  28653  colinearalg  28967  axeuclid  29020  axcontlem2  29022  axcontlem5  29025  nbgrel  29397  nbupgrres  29421  nbusgredgeu0  29425  nb3grprlem2  29438  nb3grpr2  29440  nb3gr2nb  29441  cplgr3v  29492  finsumvtxdg2ssteplem3  29605  wlkonprop  29714  upgrtrls  29757  upgristrl  29758  wksonproplem  29760  usgr2pth0  29822  wwlksnext  29950  wwlksnextsurj  29957  wwlksnfi  29963  wspthsnwspthsnon  29973  wpthswwlks2on  30021  rusgrnumwwlkl1  30028  erclwwlkref  30079  isclwwlknx  30095  clwwlknwwlksn  30097  clwwlkel  30105  erclwwlknref  30128  clwlknf1oclwwlkn  30143  clwwlknonel  30154  clwwlknon1  30156  clwwlknon2x  30162  clwwlkvbij  30172  iseupthf1o  30261  2pthfrgrrn  30341  fusgr2wsp2nb  30393  numclwwlk1lem2f1  30416  numclwwlkovh  30432  numclwlk2lem2f1o  30438  frgrregord013  30454  avril1  30522  islno  30813  h2hlm  31040  hcau  31244  hhsssh2  31330  dfch2  31467  elcnop  31917  ellnop  31918  elhmop  31933  elcnfn  31942  ellnfn  31943  dmadjss  31947  adjeu  31949  adjval  31950  hhcno  31964  hhcnf  31965  eleigvec  32017  isst  32273  ishst  32274  cvnbtwn3  32348  cvnbtwn4  32349  chirredi  32454  sumdmdii  32475  an52ds  32510  an62ds  32511  an72ds  32512  an82ds  32513  or3di  32517  rexunirn  32550  rmoun  32552  dmrab  32555  difrab2  32556  iunin1f  32616  disjunsn  32653  opeldifid  32658  ofpreima  32727  mpomptxf  32740  fdifsupp  32747  1stpreima  32769  2ndpreima  32770  f1od2  32781  resf1o  32792  maprnin  32793  nndiffz1  32849  ismnt  33048  mgcval  33052  erler  33331  opprnsg  33549  1arithidom  33602  1arithufdlem4  33612  extdgfialglem1  33842  smatrcl  33946  ordtconnlem1  34074  isrrext  34150  sigaex  34260  sigaval  34261  omssubaddlem  34449  omssubadd  34450  eulerpartleme  34513  eulerpartlemt0  34519  eulerpartlemr  34524  eulerpartlemn  34531  probun  34569  ballotlemelo  34638  ballotlem2  34639  ballotlemfc0  34643  ballotlemfcc  34644  reprdifc  34777  bnj248  34849  bnj250  34850  bnj268  34858  bnj312  34861  bnj945  34922  bnj110  35006  bnj849  35073  bnj882  35074  bnj893  35076  bnj916  35081  bnj983  35099  bnj1040  35120  bnj1175  35152  cusgredgex  35310  cusgr3cyclex  35324  erdszelem1  35379  iscvm  35447  elmpst  35724  mpstrcl  35729  dfso3  35908  xpab  35914  coepr  35941  dfdm5  35961  dfrn5  35962  elima4  35964  fv1stcnv  35965  fv2ndcnv  35966  brpprod  36071  dfon3  36078  elfix  36089  dffix2  36091  elfuns  36101  brimg  36123  brapply  36124  lemsuccf  36127  funpartlem  36130  funpartfun  36131  brrestrict  36137  dfrecs2  36138  dfrdg4  36139  lineunray  36335  ellines  36340  rmoeqi  36375  reueqi  36377  itgeq12i  36394  finminlem  36506  fneval  36540  neibastop3  36550  eliminable-abelv  37174  bj-inrab  37232  bj-axseprep  37379  bj-rest10  37398  bj-restpw  37402  bj-restuni  37407  bj-mpomptALT  37429  copsex2gd  37450  bj-imdirco  37502  icorempo  37663  isbasisrelowllem1  37667  isbasisrelowllem2  37668  relowlpssretop  37676  pibt2  37729  wl-ifp-ncond2  37777  wl-df3-3mintru2  37798  wl-2mintru1  37802  rabiun  37905  iundif1  37906  lindsenlbs  37927  poimirlem4  37936  poimirlem25  37957  poimirlem26  37958  poimirlem29  37961  poimirlem30  37962  ismblfin  37973  ovoliunnfl  37974  voliunnfl  37976  volsupnfl  37977  itg2addnclem2  37984  itg2addnclem3  37985  itg2addnc  37986  ftc1anc  38013  isbnd2  38095  bndss  38098  heibor1lem  38121  heibor1  38122  isrngohom  38277  isidl  38326  sbccom2lem  38436  anan  38547  eqbrb  38551  eqelb  38553  br1cnvinxp  38571  eldmqsres  38605  idinxpssinxp2  38636  moantr  38684  inxpxrn  38730  blockadjliftmap  38770  dfcoss3  38816  cocossss  38838  ressn2  38844  br1cossinidres  38851  br1cossincnvepres  38852  br1cossxrnidres  38853  br1cossxrncnvepres  38854  refrelcoss2  38866  symrelcoss2  38868  cosscnvssid5  38880  br1cossxrncnvssrres  38900  dfrefrel3  38908  dfcnvrefrel3  38923  cosselcnvrefrels2  38930  cosselcnvrefrels3  38931  cosselcnvrefrels4  38932  cosselcnvrefrels5  38933  dfsymrel3  38946  refsymrel2  38963  refsymrel3  38964  elrefsymrels3  38966  dftrrel3  38974  dfeqvrel2  38986  dfeqvrel3  38987  redundpbi1  39027  refrelredund3  39033  eldmqs1cossres  39056  dffunALTV2  39085  dffunALTV3  39086  dffunALTV4  39087  dffunALTV5  39088  dfdisjALTV  39110  dfdisjALTV2  39111  dfdisjALTV3  39112  dfdisjALTV4  39113  disjimdmqseq  39121  eldisjs3  39133  eldisjs4  39134  disjsuc  39171  prtlem70  39294  prtlem100  39296  prter2  39318  lsateln0  39432  islshpat  39454  lcvnbtwn3  39465  islfl  39497  ishlat1  39789  ishlat2  39790  cvrat4  39880  islvol5  40016  psubspset  40181  snatpsubN  40187  dalawlem13  40320  psubclsetN  40373  isltrn2N  40557  cdlemftr3  41002  dibelval3  41584  dicval2  41616  dicopelval2  41618  dicelval2N  41619  dihglb2  41779  islpolN  41920  lcfls1c  41973  mapdvalc  42066  mapdval4N  42069  mapdordlem1a  42071  aks4d1p8  42518  fimgmcyc  42978  prjsperref  43038  prjspeclsp  43044  elmzpcl  43157  mzpindd  43177  fphpd  43247  pw2f1ocnv  43468  islmodfg  43500  islssfg2  43502  dflim6  43695  onsucf1olem  43701  omge2  43729  tfsconcatlem  43767  tfsconcat0i  43776  rp-isfinite6  43948  minregex  43964  elmapintrab  44006  elinintrab  44007  relintab  44013  dfrtrcl5  44059  fsovrfovd  44439  ntrk1k3eqk13  44480  gneispace3  44563  k0004lem1  44577  pm13.192  44840  opelopab4  44981  ax6e2nd  44988  en3lplem2VD  45273  ax6e2ndVD  45337  ax6e2ndALT  45359  permaxrep  45436  iuneq1i  45518  ssrabf  45547  limcrecl  46063  dvnprodlem2  46379  fourierdlem103  46641  fourierdlem104  46642  4an21  47704  sprvalpwn0  47917  pairreueq  47944  dfvopnbgr2  48287  isubgredg  48300  xpsnopab  48591  sgrp2sgrp  48662  mpomptx2  48769  lindslinindsimp1  48891  lindslinindsimp2  48897  itsclc0b  49206  mo0sn  49249  coxp  49266  isthincd2  49870  thinccic  49904  2arwcatlem1  50028  setc1onsubc  50035  alsconv  50223  aacllem  50234