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  1519  19.26-3an  1904  sb3an  2117  eeeanv  2379  sbel2x  2503  rexcomf  3301  cbvreu  3404  rabeqi  3425  rabrabi  3430  rabrab  3435  ceqsex3v  3502  spc2ed  3555  rexrab  3653  reurab  3658  rmo3f  3691  reuind  3710  rmo3  3835  ssrab  3996  elin3  4103  inass  4124  rexin  4147  rexun  4194  dfun2  4215  inrab2  4262  rabun2  4269  reuun2  4270  undif4  4419  rexdifpr  4619  rexsns  4631  rexdifsn  4756  2ralunsn  4854  iuncom4  4959  iindif1  5034  iunxiun  5056  disjxun  5100  zfrep4  5245  inuni  5310  reusv2lem4  5362  reusv2  5364  otth2  5451  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  copsex2g  5464  copsex4g  5466  vopelopabsb  5502  rabxp  5698  opeliunxp  5717  opeliun2xp  5718  xpundir  5720  xpiundi  5721  xpiundir  5722  brinxp2  5728  copsex2gb  5783  cnvopab  6130  dminss  6142  imainss  6143  difxp  6154  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  33094  an62ds  33095  an72ds  33096  an82ds  33097  or3di  33099  rexunirn  33130  rmoun  33132  dmrab  33135  difrab2  33136  iunin1f  33194  disjunsn  33230  opeldifid  33235  ofpreima  33301  mpomptxf  33314  fdifsupp  33320  1stpreima  33342  2ndpreima  33343  f1od2  33353  resf1o  33364  maprnin  33365  nndiffz1  33420  ismnt  33586  mgcval  33590  erler  33868  opprnsg  34050  1arithidom  34111  1arithufdlem4  34121  extdgfialglem1  34366  smatrcl  34470  ordtconnlem1  34598  isrrext  34674  sigaex  34784  sigaval  34785  omssubaddlem  34973  omssubadd  34974  eulerpartleme  35037  eulerpartlemt0  35043  eulerpartlemr  35048  eulerpartlemn  35055  probun  35093  ballotlemelo  35162  ballotlem2  35163  ballotlemfc0  35167  ballotlemfcc  35168  reprdifc  35298  bnj248  35373  bnj250  35374  bnj268  35382  bnj312  35385  bnj945  35446  bnj110  35530  bnj849  35597  bnj882  35598  bnj893  35600  bnj916  35605  bnj983  35623  bnj1040  35644  bnj1175  35676  cusgredgex  35948  cusgr3cyclex  35953  erdszelem1  35998  iscvm  36066  elmpst  36343  mpstrcl  36348  dfso3  36527  xpab  36533  coepr  36560  dfdm5  36579  dfrn5  36580  elima4  36582  fv1stcnv  36583  fv2ndcnv  36584  brpprod  36689  dfon3  36696  elfix  36707  dffix2  36709  elfuns  36719  brimg  36741  brapply  36742  lemsuccf  36745  funpartlem  36748  funpartfun  36749  brrestrict  36755  dfrecs2  36756  dfrdg4  36757  lineunray  36954  ellines  36959  rmoeqi  37018  reueqi  37020  itgeq12i  37037  finminlem  37148  fneval  37182  neibastop3  37192  eliminable-abelv  37823  bj-inrab  37882  coi1in  38003  bj-axseprep  38032  bj-rest10  38051  bj-restpw  38055  bj-restuni  38060  bj-mpomptALT  38083  copsex2gd  38102  bj-imdirco  38154  icorempo  38317  isbasisrelowllem1  38321  isbasisrelowllem2  38322  relowlpssretop  38330  pibt2  38383  wl-ifp-ncond2  38431  wl-df3-3mintru2  38452  wl-2mintru1  38456  rabiun  38564  iundif1  38565  poimirlem4  38585  poimirlem25  38606  poimirlem26  38607  poimirlem29  38610  poimirlem30  38611  ismblfin  38622  ovoliunnfl  38623  voliunnfl  38625  volsupnfl  38626  itg2addnclem2  38633  itg2addnclem3  38634  itg2addnc  38635  ftc1anc  38662  negprop  38686  isbnd2  38760  bndss  38763  heibor1lem  38786  heibor1  38787  isrngohom  38942  isidl  38991  sbccom2lem  39099  anan  39210  eqbrb  39214  eqelb  39216  br1cnvinxp  39234  eldmqsres  39268  idinxpssinxp2  39299  moantr  39347  inxpxrn  39393  blockadjliftmap  39433  dfcoss3  39479  cocossss  39501  ressn2  39507  br1cossinidres  39514  br1cossincnvepres  39515  br1cossxrnidres  39516  br1cossxrncnvepres  39517  refrelcoss2  39529  symrelcoss2  39531  cosscnvssid5  39543  br1cossxrncnvssrres  39563  dfrefrel3  39571  dfcnvrefrel3  39586  cosselcnvrefrels2  39593  cosselcnvrefrels3  39594  cosselcnvrefrels4  39595  cosselcnvrefrels5  39596  dfsymrel3  39609  refsymrel2  39626  refsymrel3  39627  elrefsymrels3  39629  dftrrel3  39637  dfeqvrel2  39649  dfeqvrel3  39650  redundpbi1  39690  refrelredund3  39696  eldmqs1cossres  39719  dffunALTV2  39748  dffunALTV3  39749  dffunALTV4  39750  dffunALTV5  39751  dfdisjALTV  39773  dfdisjALTV2  39774  dfdisjALTV3  39775  dfdisjALTV4  39776  disjimdmqseq  39784  eldisjs3  39796  eldisjs4  39797  disjsuc  39834  prtlem70  39957  prtlem100  39959  prter2  39981  lsateln0  40095  islshpat  40117  lcvnbtwn3  40128  islfl  40160  ishlat1  40452  ishlat2  40453  cvrat4  40543  islvol5  40679  psubspset  40844  snatpsubN  40850  dalawlem13  40983  psubclsetN  41036  isltrn2N  41220  cdlemftr3  41665  dibelval3  42247  dicval2  42279  dicopelval2  42281  dicelval2N  42282  dihglb2  42442  islpolN  42583  lcfls1c  42636  mapdvalc  42729  mapdval4N  42732  mapdordlem1a  42734  aks4d1p8  43180  fimgmcyc  43641  prjsperref  43677  prjspeclsp  43683  elmzpcl  43780  mzpindd  43800  fphpd  43866  pw2f1ocnv  44087  islmodfg  44114  islssfg2  44116  dflim6  44309  onsucf1olem  44315  omge2  44343  tfsconcatlem  44381  tfsconcat0i  44390  rp-isfinite6  44562  minregex  44578  elmapintrab  44620  elinintrab  44621  relintab  44627  dfrtrcl5  44672  fsovrfovd  45052  ntrk1k3eqk13  45093  gneispace3  45176  k0004lem1  45190  pm13.192  45437  opelopab4  45577  ax6e2nd  45584  en3lplem2VD  45869  ax6e2ndVD  45933  ax6e2ndALT  45955  permaxrep  46039  iuneq1i  46144  ssrabf  46172  limcrecl  46684  dvnprodlem2  47000  fourierdlem103  47262  fourierdlem104  47263  4an21  48383  sprvalpwn0  48608  pairreueq  48635  dfvopnbgr2  48994  isubgredg  49007  xpsnopab  49298  sgrp2sgrp  49368  mpomptx2  49490  lindslinindsimp1  49612  lindslinindsimp2  49618  itsclc0b  49927  mo0sn  49969  coxp  49986  isthincd2  50588  thinccic  50622  2arwcatlem1  50746  setc1onsubc  50753  alsanmo  50949  ralsanmo  50950  alsralrex  50951  aacllem  50982