Theorem anbi1i 636

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi2ci  637  bianbi  639  anandi  689  3an4anass  1122  3ioran  1123  4anpull2OLD  1383  an33rean  1514  an42ds  1520  19.26-3an  1905  sb3an  2118  eeeanv  2380  sbel2x  2504  rexcomf  3302  cbvreu  3405  rabeqi  3426  rabrabi  3431  rabrab  3436  ceqsex3v  3503  spc2ed  3556  rexrab  3654  reurab  3659  rmo3f  3692  reuind  3711  rmo3  3836  ssrab  4019  rexun  4142  elin3  4152  inass  4173  rexin  4196  dfun2  4216  inrab2  4263  rabun2  4270  reuun2  4271  undif4  4420  rexdifpr  4620  rexsns  4632  rexdifsn  4757  2ralunsn  4855  iuncom4  4960  iindif1  5035  iunxiun  5057  disjxun  5101  zfrep4  5246  inuni  5311  reusv2lem4  5363  reusv2  5365  otth2  5452  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  copsex2g  5465  copsex4g  5467  vopelopabsb  5503  rabxp  5699  opeliunxp  5718  opeliun2xp  5719  xpundir  5721  xpiundi  5722  xpiundir  5723  brinxp2  5729  copsex2gb  5784  cnvopab  6131  dminss  6143  imainss  6144  difxp  6155  cnvresima  6231  coundi  6248  resco  6251  imaco  6252  rnco  6253  rncoOLD  6254  coiun  6258  coi1  6264  coass  6267  cnvpo  6290  xpco  6292  dfpo2  6299  frpoind  6345  dffun2  6548  fncnv  6613  imadif  6624  mptun  6685  ffrnb  6724  dff1o2  6830  dff1o3  6831  brprcneu  6875  brprcneuALT  6876  fvun2  6977  eqfnfv3  7031  respreima  7065  f1ompt  7111  f1ossf1o  7129  fsn  7136  fmptsng  7173  fmptsnd  7174  tpres  7207  abrexco  7248  imaiun  7249  f1mpt  7265  dff1o6  7283  riotarab  7419  oprabidw  7451  oprabid  7452  dfoprab2  7478  oprab4  7506  mpomptx  7533  mpt3mpt  7685  elpwpwel  7781  elxp4  7934  elxp5  7935  ffoss  7958  f11o  7959  opabex3d  7977  opabex3rd  7978  opabex3  7979  abexssex  7982  elxp7  8036  dfopab2  8063  dfoprab3s  8064  fsplit  8128  frxp  8138  xporderlem  8139  frpoins3xp3g  8158  soseq  8176  suppssov1  8214  suppssov2  8215  suppssfv  8219  brtpos2  8249  tpostpos  8263  tposmpo  8280  dfrecs3  8380  oarec  8570  oeeu  8612  eldifsucnn  8673  naddasslem1  8704  mapsncnv  8921  dfixp  8927  domen  8988  xpsnen  9080  xpcomco  9086  xpassen  9090  sbthlem9  9114  frfi  9276  marypha2lem2  9428  brttrcl2  9715  epfrs  9732  tcsni  9742  frind  9754  cp  9954  dfac5lem1  10202  dfac5lem2  10203  dfac5lem5  10206  kmlem3  10231  dfackm  10245  cfval2  10338  cflim3  10340  cfss  10343  cfslb  10344  zfcndrep  10699  eltsk2g  10836  ltexpi  10987  recmulnq  11049  ltexprlem4  11124  addsrpr  11160  mulsrpr  11161  addcnsr  11220  mulcnsr  11221  ltresr  11225  axrrecex  11248  elnnz  12703  elnn0z  12706  fnn0ind  12798  rexuz2  13026  rexrp  13143  elixx3g  13489  elfz2  13646  elfzuzb  13650  fznn  13726  elfz2nn0  13752  fznn0  13753  4fvwrd4  13782  preduz  13784  elfzo2  13796  fzind2  13923  hashgt23el  14569  hashf1lem1  14600  hashf1lem2  14601  fz1isolem  14606  s4f1o  15069  wwlktovfo  15111  fsum2dlem  15936  modfsummod  15961  prodeq1i  16085  sinltx  16357  divalglem10  16572  divalgb  16574  coprmproddvdslem  16837  isprm2  16857  infpn2  17091  prdsle  17633  prdsless  17634  prdsleval  17648  imasleval  17713  xpscf  17737  dfiso2  17947  oppcsect  17953  elhoma  18207  ispos2  18489  lubeldm  18525  glbeldm  18538  tosso  18591  ismgmhm  18885  issubmgm  18891  submgmacs  18906  ismhm  18980  issubm  18998  submacs  19023  issubg  19336  issubg3  19355  gaorb  19521  pmtrrn2  19674  efgcpbllema  19968  efgcpbllemb  19969  frgpuplem  19986  imasabl  20090  subgdmdprd  20250  dprd2d2  20260  omndmul2  20347  dfring3  20518  dfrhm2  20704  isrhm0  20706  opprnzrb  20772  issubrg  20823  isdomn3  20966  drngprop  20998  drngid2  21010  opprdrng  21021  isabv  21068  isorng  21118  islss  21209  islbs  21351  lsmspsn  21359  isobs  22026  islinds  22115  lindsenlbs  22157  isassa  22164  aspval2  22206  ltbval  22352  opsrle  22356  opsrtoslem1  22364  fvmptnn04if  23167  ntreq0  23395  restntr  23500  cnnei  23600  hausnei2  23671  cmpcov2  23708  cmpsub  23718  uncmp  23721  cmpfi  23726  llyi  23793  dissnlocfin  23848  iskgen3  23868  1stckgenlem  23872  ptpjpre1  23890  txcnpi  23927  txtube  23959  hausdiag  23964  txlm  23967  txkgen  23971  cfinfil  24212  csdfil  24213  supfil  24214  fin1aufil  24251  elflim2  24283  hauspwpwf1  24306  txflf  24325  isfcls  24328  alexsubALTlem3  24368  alexsubALT  24370  cnextcn  24386  istmd  24393  istgp  24396  tgphaus  24436  qustgplem  24440  istrg  24483  istdrg  24485  istlm  24504  blres  24750  isms2  24769  metrest  24843  metuel2  24884  restmetu  24889  isngp  24915  isnlm  24994  elii1  25256  isclmp  25418  iscvsp  25449  isncvsngp  25470  iscph  25491  cfilucfil3  25641  isbn  25659  limcrcl  26194  ig1pval3  26496  plydivex  26618  ellogdm  26967  cubic  27177  dmarea  27285  vmasum  27543  lgsquadlem2  27708  elno3  28012  lenlts  28109  madeval2  28219  elnnzs  28787  istrkg3ld  28923  legov  29048  ltgov  29060  colinearalg  29488  axeuclid  29541  axcontlem2  29543  axcontlem5  29546  nbgrel  29921  nbupgrres  29945  nbusgredgeu0  29949  nb3grprlem2  29962  nb3grpr2  29964  nb3gr2nb  29965  cplgr3v  30016  finsumvtxdg2ssteplem3  30128  wlkonprop  30237  upgrtrls  30284  upgristrl  30285  wksonproplem  30287  usgr2pth0  30351  wwlksnext  30482  wwlksnextsurj  30489  wwlksnfi  30495  wspthsnwspthsnon  30505  wpthswwlks2on  30553  rusgrnumwwlkl1  30560  erclwwlkref  30611  isclwwlknx  30627  clwwlknwwlksn  30629  clwwlkel  30637  erclwwlknref  30660  clwlknf1oclwwlkn  30675  clwwlknonel  30686  clwwlknon1  30688  clwwlknon2x  30694  clwwlkvbij  30704  iseupthf1o  30803  2pthfrgrrn  30883  fusgr2wsp2nb  30935  numclwwlk1lem2f1  30958  numclwwlkovh  30974  numclwlk2lem2f1o  30980  frgrregord013  30996  avril1  31064  islno  31355  h2hlm  31582  hcau  31786  hhsssh2  31872  dfch2  32009  elcnop  32459  ellnop  32460  elhmop  32475  elcnfn  32484  ellnfn  32485  dmadjss  32489  adjeu  32491  adjval  32492  hhcno  32506  hhcnf  32507  eleigvec  32559  isst  32815  ishst  32816  cvnbtwn3  32890  cvnbtwn4  32891  chirredi  32996  sumdmdii  33017  an52ds  33052  an62ds  33053  an72ds  33054  an82ds  33055  or3di  33057  rexunirn  33088  rmoun  33090  dmrab  33093  difrab2  33094  iunin1f  33152  disjunsn  33188  opeldifid  33193  ofpreima  33259  mpomptxf  33272  fdifsupp  33278  1stpreima  33300  2ndpreima  33301  f1od2  33311  resf1o  33322  maprnin  33323  nndiffz1  33378  ismnt  33544  mgcval  33548  erler  33826  opprnsg  34008  1arithidom  34069  1arithufdlem4  34079  extdgfialglem1  34324  smatrcl  34428  ordtconnlem1  34556  isrrext  34632  sigaex  34742  sigaval  34743  omssubaddlem  34931  omssubadd  34932  eulerpartleme  34995  eulerpartlemt0  35001  eulerpartlemr  35006  eulerpartlemn  35013  probun  35051  ballotlemelo  35120  ballotlem2  35121  ballotlemfc0  35125  ballotlemfcc  35126  reprdifc  35256  bnj248  35331  bnj250  35332  bnj268  35340  bnj312  35343  bnj945  35404  bnj110  35488  bnj849  35555  bnj882  35556  bnj893  35558  bnj916  35563  bnj983  35581  bnj1040  35602  bnj1175  35634  cusgredgex  35906  cusgr3cyclex  35911  erdszelem1  35956  iscvm  36024  elmpst  36301  mpstrcl  36306  dfso3  36485  xpab  36491  coepr  36518  dfdm5  36537  dfrn5  36538  elima4  36540  fv1stcnv  36541  fv2ndcnv  36542  brpprod  36647  dfon3  36654  elfix  36665  dffix2  36667  elfuns  36677  brimg  36699  brapply  36700  lemsuccf  36703  funpartlem  36706  funpartfun  36707  brrestrict  36713  dfrecs2  36714  dfrdg4  36715  lineunray  36912  ellines  36917  rmoeqi  36976  reueqi  36978  itgeq12i  36995  finminlem  37106  fneval  37140  neibastop3  37150  eliminable-abelv  37781  bj-inrab  37840  coi1in  37961  bj-axseprep  37990  bj-rest10  38009  bj-restpw  38013  bj-restuni  38018  bj-mpomptALT  38040  copsex2gd  38059  bj-imdirco  38111  icorempo  38274  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlpssretop  38287  pibt2  38340  wl-ifp-ncond2  38388  wl-df3-3mintru2  38409  wl-2mintru1  38413  rabiun  38521  iundif1  38522  poimirlem4  38542  poimirlem25  38563  poimirlem26  38564  poimirlem29  38567  poimirlem30  38568  ismblfin  38579  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  itg2addnclem2  38590  itg2addnclem3  38591  itg2addnc  38592  ftc1anc  38619  negprop  38643  isbnd2  38717  bndss  38720  heibor1lem  38743  heibor1  38744  isrngohom  38899  isidl  38948  sbccom2lem  39056  anan  39167  eqbrb  39171  eqelb  39173  br1cnvinxp  39191  eldmqsres  39225  idinxpssinxp2  39256  moantr  39304  inxpxrn  39350  blockadjliftmap  39390  dfcoss3  39436  cocossss  39458  ressn2  39464  br1cossinidres  39471  br1cossincnvepres  39472  br1cossxrnidres  39473  br1cossxrncnvepres  39474  refrelcoss2  39486  symrelcoss2  39488  cosscnvssid5  39500  br1cossxrncnvssrres  39520  dfrefrel3  39528  dfcnvrefrel3  39543  cosselcnvrefrels2  39550  cosselcnvrefrels3  39551  cosselcnvrefrels4  39552  cosselcnvrefrels5  39553  dfsymrel3  39566  refsymrel2  39583  refsymrel3  39584  elrefsymrels3  39586  dftrrel3  39594  dfeqvrel2  39606  dfeqvrel3  39607  redundpbi1  39647  refrelredund3  39653  eldmqs1cossres  39676  dffunALTV2  39705  dffunALTV3  39706  dffunALTV4  39707  dffunALTV5  39708  dfdisjALTV  39730  dfdisjALTV2  39731  dfdisjALTV3  39732  dfdisjALTV4  39733  disjimdmqseq  39741  eldisjs3  39753  eldisjs4  39754  disjsuc  39791  prtlem70  39914  prtlem100  39916  prter2  39938  lsateln0  40052  islshpat  40074  lcvnbtwn3  40085  islfl  40117  ishlat1  40409  ishlat2  40410  cvrat4  40500  islvol5  40636  psubspset  40801  snatpsubN  40807  dalawlem13  40940  psubclsetN  40993  isltrn2N  41177  cdlemftr3  41622  dibelval3  42204  dicval2  42236  dicopelval2  42238  dicelval2N  42239  dihglb2  42399  islpolN  42540  lcfls1c  42593  mapdvalc  42686  mapdval4N  42689  mapdordlem1a  42691  aks4d1p8  43137  fimgmcyc  43598  prjsperref  43634  prjspeclsp  43640  elmzpcl  43736  mzpindd  43756  fphpd  43822  pw2f1ocnv  44043  islmodfg  44070  islssfg2  44072  dflim6  44265  onsucf1olem  44271  omge2  44299  tfsconcatlem  44337  tfsconcat0i  44346  rp-isfinite6  44518  minregex  44534  elmapintrab  44576  elinintrab  44577  relintab  44583  dfrtrcl5  44628  fsovrfovd  45008  ntrk1k3eqk13  45049  gneispace3  45132  k0004lem1  45146  pm13.192  45393  opelopab4  45533  ax6e2nd  45540  en3lplem2VD  45825  ax6e2ndVD  45889  ax6e2ndALT  45911  permaxrep  45995  iuneq1i  46100  ssrabf  46128  limcrecl  46640  dvnprodlem2  46956  fourierdlem103  47218  fourierdlem104  47219  4an21  48339  sprvalpwn0  48564  pairreueq  48591  dfvopnbgr2  48950  isubgredg  48963  xpsnopab  49254  sgrp2sgrp  49324  mpomptx2  49446  lindslinindsimp1  49568  lindslinindsimp2  49574  itsclc0b  49883  mo0sn  49925  coxp  49942  isthincd2  50544  thinccic  50578  2arwcatlem1  50702  setc1onsubc  50709  alsanmo  50905  ralsanmo  50906  alsralrex  50907  aacllem  50938