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  3393  rabeqi  3414  rabrabi  3420  rabrab  3425  ceqsex3v  3497  spc2ed  3557  rexrab  3656  reurab  3661  rmo3f  3694  reuind  3713  rmo3  3841  ssrab  4025  rexun  4150  elin3  4160  inass  4182  rexin  4204  dfun2  4224  inrab2  4271  rabun2  4278  reuun2  4279  undif4  4421  rexdifpr  4618  rexsns  4630  rexdifsn  4752  2ralunsn  4853  iuncom4  4957  iindif1  5032  iunxiun  5054  disjxun  5098  zfrep4  5240  inuni  5297  reusv2lem4  5348  reusv2  5350  otth2  5439  copsexgw  5446  copsexg  5447  copsex2g  5449  copsex4g  5451  vopelopabsb  5485  rabxp  5680  opeliunxp  5699  opeliun2xp  5700  xpundir  5702  xpiundi  5703  xpiundir  5704  brinxp2  5710  copsex2gb  5763  cnvopab  6102  dminss  6119  imainss  6120  difxp  6130  cnvresima  6196  coundi  6213  resco  6216  imaco  6217  rnco  6218  rncoOLD  6219  coiun  6223  coi1  6229  coass  6232  cnvpo  6253  xpco  6255  dfpo2  6262  frpoind  6308  dffun2  6510  fncnv  6573  imadif  6584  mptun  6646  ffrnb  6684  dff1o2  6787  dff1o3  6788  brprcneu  6832  brprcneuALT  6833  fvun2  6934  eqfnfv3  6987  respreima  7020  f1ompt  7065  f1ossf1o  7083  fsn  7090  fmptsng  7124  fmptsnd  7125  tpres  7157  abrexco  7200  imaiun  7201  f1mpt  7217  dff1o6  7231  imaeqsexvOLD  7319  riotarab  7367  oprabidw  7399  oprabid  7400  dfoprab2  7426  oprab4  7454  mpomptx  7481  elpwpwel  7722  elxp4  7874  elxp5  7875  ffoss  7900  f11o  7901  opabex3d  7919  opabex3rd  7920  opabex3  7921  abexssex  7924  elxp7  7978  dfopab2  8006  dfoprab3s  8007  fsplit  8069  frxp  8078  xporderlem  8079  frpoins3xp3g  8093  soseq  8111  suppssov1  8149  suppssov2  8150  suppssfv  8154  brtpos2  8184  tpostpos  8198  tposmpo  8215  dfrecs3  8314  oarec  8499  oeeu  8541  eldifsucnn  8602  naddasslem1  8632  mapsncnv  8843  dfixp  8849  domen  8910  xpsnen  9001  xpcomco  9007  xpassen  9011  sbthlem9  9035  frfi  9197  marypha2lem2  9351  brttrcl2  9635  epfrs  9652  tcsni  9662  frind  9674  cp  9815  dfac5lem1  10045  dfac5lem2  10046  dfac5lem5  10049  kmlem3  10075  dfackm  10089  cfval2  10182  cflim3  10184  cfss  10187  cfslb  10188  zfcndrep  10537  eltsk2g  10674  ltexpi  10825  recmulnq  10887  ltexprlem4  10962  addsrpr  10998  mulsrpr  10999  addcnsr  11058  mulcnsr  11059  ltresr  11063  axrrecex  11086  elnnz  12510  elnn0z  12513  fnn0ind  12603  rexuz2  12824  rexrp  12940  elixx3g  13286  elfz2  13442  elfzuzb  13446  fznn  13520  elfz2nn0  13546  fznn0  13547  4fvwrd4  13576  preduz  13578  elfzo2  13590  fzind2  13716  hashgt23el  14359  hashf1lem1  14390  hashf1lem2  14391  fz1isolem  14396  s4f1o  14853  wwlktovfo  14893  fsum2dlem  15705  modfsummod  15729  prodeq1i  15851  sinltx  16126  divalglem10  16341  divalgb  16343  coprmproddvdslem  16601  isprm2  16621  infpn2  16853  prdsle  17394  prdsless  17395  prdsleval  17409  imasleval  17474  xpscf  17498  dfiso2  17708  oppcsect  17714  elhoma  17968  ispos2  18250  lubeldm  18286  glbeldm  18299  tosso  18352  ismgmhm  18633  issubmgm  18639  submgmacs  18654  ismhm  18722  issubm  18740  submacs  18764  issubg  19068  issubg3  19086  gaorb  19248  pmtrrn2  19401  efgcpbllema  19695  efgcpbllemb  19696  frgpuplem  19713  imasabl  19817  subgdmdprd  19977  dprd2d2  19987  omndmul2  20074  dfrhm2  20422  opprnzrb  20466  issubrg  20516  isdomn3  20660  drngprop  20689  drngid2  20697  opprdrng  20709  isabv  20756  isorng  20806  islss  20897  islbs  21040  lsmspsn  21048  isobs  21687  islinds  21776  isassa  21823  aspval2  21866  ltbval  22010  opsrle  22014  opsrtoslem1  22022  fvmptnn04if  22805  ntreq0  23033  restntr  23138  cnnei  23238  hausnei2  23309  cmpcov2  23346  cmpsub  23356  uncmp  23359  cmpfi  23364  llyi  23430  dissnlocfin  23485  iskgen3  23505  1stckgenlem  23509  ptpjpre1  23527  txcnpi  23564  txtube  23596  hausdiag  23601  txlm  23604  txkgen  23608  cfinfil  23849  csdfil  23850  supfil  23851  fin1aufil  23888  elflim2  23920  hauspwpwf1  23943  txflf  23962  isfcls  23965  alexsubALTlem3  24005  alexsubALT  24007  cnextcn  24023  istmd  24030  istgp  24033  tgphaus  24073  qustgplem  24077  istrg  24120  istdrg  24122  istlm  24141  blres  24387  isms2  24406  metrest  24480  metuel2  24521  restmetu  24526  isngp  24552  isnlm  24631  elii1  24899  isclmp  25065  iscvsp  25096  isncvsngp  25117  iscph  25138  cfilucfil3  25288  isbn  25306  limcrcl  25843  ig1pval3  26151  plydivex  26273  ellogdm  26616  cubic  26827  dmarea  26935  vmasum  27195  lgsquadlem1  27359  lgsquadlem2  27360  elno3  27635  lenlts  27732  madeval2  27841  elnnzs  28409  istrkg3ld  28545  legov  28669  ltgov  28681  colinearalg  28995  axeuclid  29048  axcontlem2  29050  axcontlem5  29053  nbgrel  29425  nbupgrres  29449  nbusgredgeu0  29453  nb3grprlem2  29466  nb3grpr2  29468  nb3gr2nb  29469  cplgr3v  29520  finsumvtxdg2ssteplem3  29633  wlkonprop  29742  upgrtrls  29785  upgristrl  29786  wksonproplem  29788  usgr2pth0  29850  wwlksnext  29978  wwlksnextsurj  29985  wwlksnfi  29991  wspthsnwspthsnon  30001  wpthswwlks2on  30049  rusgrnumwwlkl1  30056  erclwwlkref  30107  isclwwlknx  30123  clwwlknwwlksn  30125  clwwlkel  30133  erclwwlknref  30156  clwlknf1oclwwlkn  30171  clwwlknonel  30182  clwwlknon1  30184  clwwlknon2x  30190  clwwlkvbij  30200  iseupthf1o  30289  2pthfrgrrn  30369  fusgr2wsp2nb  30421  numclwwlk1lem2f1  30444  numclwwlkovh  30460  numclwlk2lem2f1o  30466  frgrregord013  30482  avril1  30550  islno  30841  h2hlm  31068  hcau  31272  hhsssh2  31358  dfch2  31495  elcnop  31945  ellnop  31946  elhmop  31961  elcnfn  31970  ellnfn  31971  dmadjss  31975  adjeu  31977  adjval  31978  hhcno  31992  hhcnf  31993  eleigvec  32045  isst  32301  ishst  32302  cvnbtwn3  32376  cvnbtwn4  32377  chirredi  32482  sumdmdii  32503  an52ds  32538  an62ds  32539  an72ds  32540  an82ds  32541  or3di  32545  rexunirn  32578  rmoun  32580  dmrab  32583  difrab2  32584  iunin1f  32644  disjunsn  32681  opeldifid  32686  ofpreima  32755  mpomptxf  32768  fdifsupp  32775  1stpreima  32797  2ndpreima  32798  f1od2  32809  resf1o  32820  maprnin  32821  nndiffz1  32877  ismnt  33076  mgcval  33080  erler  33359  opprnsg  33577  1arithidom  33630  1arithufdlem4  33640  extdgfialglem1  33870  smatrcl  33974  ordtconnlem1  34102  isrrext  34178  sigaex  34288  sigaval  34289  omssubaddlem  34477  omssubadd  34478  eulerpartleme  34541  eulerpartlemt0  34547  eulerpartlemr  34552  eulerpartlemn  34559  probun  34597  ballotlemelo  34666  ballotlem2  34667  ballotlemfc0  34671  ballotlemfcc  34672  reprdifc  34805  bnj248  34877  bnj250  34878  bnj268  34886  bnj312  34889  bnj945  34950  bnj110  35034  bnj849  35101  bnj882  35102  bnj893  35104  bnj916  35109  bnj983  35127  bnj1040  35148  bnj1175  35180  cusgredgex  35338  cusgr3cyclex  35352  erdszelem1  35407  iscvm  35475  elmpst  35752  mpstrcl  35757  dfso3  35936  xpab  35942  coepr  35969  dfdm5  35989  dfrn5  35990  elima4  35992  fv1stcnv  35993  fv2ndcnv  35994  brpprod  36099  dfon3  36106  elfix  36117  dffix2  36119  elfuns  36129  brimg  36151  brapply  36152  lemsuccf  36155  funpartlem  36158  funpartfun  36159  brrestrict  36165  dfrecs2  36166  dfrdg4  36167  lineunray  36363  ellines  36368  rmoeqi  36403  reueqi  36405  itgeq12i  36422  finminlem  36534  fneval  36568  neibastop3  36578  eliminable-abelv  37117  bj-inrab  37175  bj-axseprep  37322  bj-rest10  37341  bj-restpw  37345  bj-restuni  37350  bj-mpomptALT  37372  copsex2gd  37393  bj-imdirco  37445  icorempo  37606  isbasisrelowllem1  37610  isbasisrelowllem2  37611  relowlpssretop  37619  pibt2  37672  wl-ifp-ncond2  37720  wl-df3-3mintru2  37741  wl-2mintru1  37745  rabiun  37844  iundif1  37845  lindsenlbs  37866  poimirlem4  37875  poimirlem25  37896  poimirlem26  37897  poimirlem29  37900  poimirlem30  37901  ismblfin  37912  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  itg2addnclem2  37923  itg2addnclem3  37924  itg2addnc  37925  ftc1anc  37952  isbnd2  38034  bndss  38037  heibor1lem  38060  heibor1  38061  isrngohom  38216  isidl  38265  sbccom2lem  38375  anan  38486  eqbrb  38490  eqelb  38492  br1cnvinxp  38510  eldmqsres  38544  idinxpssinxp2  38575  moantr  38623  inxpxrn  38669  blockadjliftmap  38709  dfcoss3  38755  cocossss  38777  ressn2  38783  br1cossinidres  38790  br1cossincnvepres  38791  br1cossxrnidres  38792  br1cossxrncnvepres  38793  refrelcoss2  38805  symrelcoss2  38807  cosscnvssid5  38819  br1cossxrncnvssrres  38839  dfrefrel3  38847  dfcnvrefrel3  38862  cosselcnvrefrels2  38869  cosselcnvrefrels3  38870  cosselcnvrefrels4  38871  cosselcnvrefrels5  38872  dfsymrel3  38885  refsymrel2  38902  refsymrel3  38903  elrefsymrels3  38905  dftrrel3  38913  dfeqvrel2  38925  dfeqvrel3  38926  redundpbi1  38966  refrelredund3  38972  eldmqs1cossres  38995  dffunALTV2  39024  dffunALTV3  39025  dffunALTV4  39026  dffunALTV5  39027  dfdisjALTV  39049  dfdisjALTV2  39050  dfdisjALTV3  39051  dfdisjALTV4  39052  disjimdmqseq  39060  eldisjs3  39072  eldisjs4  39073  disjsuc  39110  prtlem70  39233  prtlem100  39235  prter2  39257  lsateln0  39371  islshpat  39393  lcvnbtwn3  39404  islfl  39436  ishlat1  39728  ishlat2  39729  cvrat4  39819  islvol5  39955  psubspset  40120  snatpsubN  40126  dalawlem13  40259  psubclsetN  40312  isltrn2N  40496  cdlemftr3  40941  dibelval3  41523  dicval2  41555  dicopelval2  41557  dicelval2N  41558  dihglb2  41718  islpolN  41859  lcfls1c  41912  mapdvalc  42005  mapdval4N  42008  mapdordlem1a  42010  aks4d1p8  42457  fimgmcyc  42904  prjsperref  42964  prjspeclsp  42970  elmzpcl  43083  mzpindd  43103  fphpd  43173  pw2f1ocnv  43394  islmodfg  43426  islssfg2  43428  dflim6  43621  onsucf1olem  43627  omge2  43655  tfsconcatlem  43693  tfsconcat0i  43702  rp-isfinite6  43874  minregex  43890  elmapintrab  43932  elinintrab  43933  relintab  43939  dfrtrcl5  43985  fsovrfovd  44365  ntrk1k3eqk13  44406  gneispace3  44489  k0004lem1  44503  pm13.192  44766  opelopab4  44907  ax6e2nd  44914  en3lplem2VD  45199  ax6e2ndVD  45263  ax6e2ndALT  45285  permaxrep  45362  iuneq1i  45444  ssrabf  45473  limcrecl  45989  dvnprodlem2  46305  fourierdlem103  46567  fourierdlem104  46568  4an21  47630  sprvalpwn0  47843  pairreueq  47870  dfvopnbgr2  48213  isubgredg  48226  xpsnopab  48517  sgrp2sgrp  48588  mpomptx2  48695  lindslinindsimp1  48817  lindslinindsimp2  48823  itsclc0b  49132  mo0sn  49175  coxp  49192  isthincd2  49796  thinccic  49830  2arwcatlem1  49954  setc1onsubc  49961  alsconv  50149  aacllem  50160