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  19.26-3an  1872  sb3an  2082  eeeanv  2348  sbel2x  2472  rexcomf  3277  cbvreu  3397  rabeqi  3419  rabrabi  3425  rabrab  3430  ceqsex3v  3503  spc2ed  3567  rexrab  3667  reurab  3672  rmo3f  3705  reuind  3724  rmo3  3852  ssrab  4036  rexun  4159  elin3  4169  inass  4191  rexin  4213  dfun2  4233  inrab2  4280  rabun2  4287  reuun2  4288  undif4  4430  rexdifpr  4623  rexsns  4635  rexdifsn  4758  2ralunsn  4859  iuncom4  4964  iindif1  5039  iunxiun  5061  disjxun  5105  zfrep4  5248  inuni  5305  reusv2lem4  5356  reusv2  5358  otth2  5443  copsexgw  5450  copsexg  5451  copsex2g  5453  copsex4g  5455  vopelopabsb  5489  rabxp  5686  opeliunxp  5705  opeliun2xp  5706  xpundir  5708  xpiundi  5709  xpiundir  5710  brinxp2  5716  copsex2gb  5769  cnvopab  6110  dminss  6126  imainss  6127  difxp  6137  cnvresima  6203  coundi  6220  resco  6223  imaco  6224  rnco  6225  coiun  6229  coi1  6235  coass  6238  cnvpo  6260  xpco  6262  dfpo2  6269  frpoind  6315  dffun2  6521  dffun2OLD  6522  dffun2OLDOLD  6523  fncnv  6589  imadif  6600  mptun  6664  ffrnb  6702  dff1o2  6805  dff1o3  6806  brprcneu  6848  brprcneuALT  6849  fvun2  6953  eqfnfv3  7005  respreima  7038  f1ompt  7083  f1ossf1o  7100  fsn  7107  fmptsng  7142  fmptsnd  7143  tpres  7175  abrexco  7218  imaiun  7219  f1mpt  7236  dff1o6  7250  imaeqsexvOLD  7338  riotarab  7386  oprabidw  7418  oprabid  7419  dfoprab2  7447  oprab4  7475  mpomptx  7502  elpwpwel  7743  elxp4  7898  elxp5  7899  ffoss  7924  f11o  7925  opabex3d  7944  opabex3rd  7945  opabex3  7946  abexssex  7949  elxp7  8003  dfopab2  8031  dfoprab3s  8032  fsplit  8096  frxp  8105  xporderlem  8106  frpoins3xp3g  8120  soseq  8138  suppssov1  8176  suppssov2  8177  suppssfv  8181  brtpos2  8211  tpostpos  8225  tposmpo  8242  dfrecs3  8341  oarec  8526  oeeu  8567  eldifsucnn  8628  naddasslem1  8658  mapsncnv  8866  dfixp  8872  domen  8933  xpsnen  9025  xpcomco  9031  xpassen  9035  sbthlem9  9059  frfi  9232  marypha2lem2  9387  brttrcl2  9667  epfrs  9684  tcsni  9696  frind  9703  cp  9844  dfac5lem1  10076  dfac5lem2  10077  dfac5lem5  10080  kmlem3  10106  dfackm  10120  cfval2  10213  cflim3  10215  cfss  10218  cfslb  10219  zfcndrep  10567  eltsk2g  10704  ltexpi  10855  recmulnq  10917  ltexprlem4  10992  addsrpr  11028  mulsrpr  11029  addcnsr  11088  mulcnsr  11089  ltresr  11093  axrrecex  11116  elnnz  12539  elnn0z  12542  fnn0ind  12633  rexuz2  12858  rexrp  12974  elixx3g  13319  elfz2  13475  elfzuzb  13479  fznn  13553  elfz2nn0  13579  fznn0  13580  4fvwrd4  13609  preduz  13611  elfzo2  13623  fzind2  13746  hashgt23el  14389  hashf1lem1  14420  hashf1lem2  14421  fz1isolem  14426  s4f1o  14884  wwlktovfo  14924  fsum2dlem  15736  modfsummod  15760  prodeq1i  15882  sinltx  16157  divalglem10  16372  divalgb  16374  coprmproddvdslem  16632  isprm2  16652  infpn2  16884  prdsle  17425  prdsless  17426  prdsleval  17440  imasleval  17504  xpscf  17528  dfiso2  17734  oppcsect  17740  elhoma  17994  ispos2  18276  lubeldm  18312  glbeldm  18325  tosso  18378  ismgmhm  18623  issubmgm  18629  submgmacs  18644  ismhm  18712  issubm  18730  submacs  18754  issubg  19058  issubg3  19076  gaorb  19239  pmtrrn2  19390  efgcpbllema  19684  efgcpbllemb  19685  frgpuplem  19702  imasabl  19806  subgdmdprd  19966  dprd2d2  19976  dfrhm2  20383  opprnzrb  20430  issubrg  20480  isdomn3  20624  drngprop  20653  drngid2  20661  opprdrng  20673  isabv  20720  islss  20840  islbs  20983  lsmspsn  20991  isobs  21629  islinds  21718  isassa  21765  aspval2  21807  ltbval  21950  opsrle  21954  opsrtoslem1  21962  fvmptnn04if  22736  ntreq0  22964  restntr  23069  cnnei  23169  hausnei2  23240  cmpcov2  23277  cmpsub  23287  uncmp  23290  cmpfi  23295  llyi  23361  dissnlocfin  23416  iskgen3  23436  1stckgenlem  23440  ptpjpre1  23458  txcnpi  23495  txtube  23527  hausdiag  23532  txlm  23535  txkgen  23539  cfinfil  23780  csdfil  23781  supfil  23782  fin1aufil  23819  elflim2  23851  hauspwpwf1  23874  txflf  23893  isfcls  23896  alexsubALTlem3  23936  alexsubALT  23938  cnextcn  23954  istmd  23961  istgp  23964  tgphaus  24004  qustgplem  24008  istrg  24051  istdrg  24053  istlm  24072  blres  24319  isms2  24338  metrest  24412  metuel2  24453  restmetu  24458  isngp  24484  isnlm  24563  elii1  24831  isclmp  24997  iscvsp  25028  isncvsngp  25049  iscph  25070  cfilucfil3  25220  isbn  25238  limcrcl  25775  ig1pval3  26083  plydivex  26205  ellogdm  26548  cubic  26759  dmarea  26867  vmasum  27127  lgsquadlem1  27291  lgsquadlem2  27292  elno3  27567  slenlt  27664  madeval2  27761  elnnzs  28289  istrkg3ld  28388  legov  28512  ltgov  28524  colinearalg  28837  axeuclid  28890  axcontlem2  28892  axcontlem5  28895  nbgrel  29267  nbupgrres  29291  nbusgredgeu0  29295  nb3grprlem2  29308  nb3grpr2  29310  nb3gr2nb  29311  cplgr3v  29362  finsumvtxdg2ssteplem3  29475  wlkonprop  29586  upgrtrls  29629  upgristrl  29630  wksonproplem  29632  wksonproplemOLD  29633  usgr2pth0  29695  wwlksnext  29823  wwlksnextsurj  29830  wwlksnfi  29836  wspthsnwspthsnon  29846  wpthswwlks2on  29891  rusgrnumwwlkl1  29898  erclwwlkref  29949  isclwwlknx  29965  clwwlknwwlksn  29967  clwwlkel  29975  erclwwlknref  29998  clwlknf1oclwwlkn  30013  clwwlknonel  30024  clwwlknon1  30026  clwwlknon2x  30032  clwwlkvbij  30042  iseupthf1o  30131  2pthfrgrrn  30211  fusgr2wsp2nb  30263  numclwwlk1lem2f1  30286  numclwwlkovh  30302  numclwlk2lem2f1o  30308  frgrregord013  30324  avril1  30392  islno  30682  h2hlm  30909  hcau  31113  hhsssh2  31199  dfch2  31336  elcnop  31786  ellnop  31787  elhmop  31802  elcnfn  31811  ellnfn  31812  dmadjss  31816  adjeu  31818  adjval  31819  hhcno  31833  hhcnf  31834  eleigvec  31886  isst  32142  ishst  32143  cvnbtwn3  32217  cvnbtwn4  32218  chirredi  32323  sumdmdii  32344  an42ds  32379  an52ds  32380  an62ds  32381  an72ds  32382  an82ds  32383  or3di  32388  rexunirn  32421  rmoun  32423  dmrab  32426  difrab2  32427  iunin1f  32486  disjunsn  32523  opeldifid  32528  ofpreima  32589  mpomptxf  32601  fdifsupp  32608  1stpreima  32630  2ndpreima  32631  f1od2  32644  resf1o  32653  maprnin  32654  nndiffz1  32709  ismnt  32909  mgcval  32913  omndmul2  33026  erler  33216  isorng  33277  opprnsg  33455  1arithidom  33508  1arithufdlem4  33518  smatrcl  33786  ordtconnlem1  33914  isrrext  33990  sigaex  34100  sigaval  34101  omssubaddlem  34290  omssubadd  34291  eulerpartleme  34354  eulerpartlemt0  34360  eulerpartlemr  34365  eulerpartlemn  34372  probun  34410  ballotlemelo  34479  ballotlem2  34480  ballotlemfc0  34484  ballotlemfcc  34485  reprdifc  34618  bnj248  34690  bnj250  34691  bnj268  34699  bnj312  34702  bnj945  34763  bnj110  34848  bnj849  34915  bnj882  34916  bnj893  34918  bnj916  34923  bnj983  34941  bnj1040  34962  bnj1175  34994  cusgredgex  35109  cusgr3cyclex  35123  erdszelem1  35178  iscvm  35246  elmpst  35523  mpstrcl  35528  dfso3  35707  xpab  35713  coepr  35740  dfdm5  35760  dfrn5  35761  elima4  35763  fv1stcnv  35764  fv2ndcnv  35765  brpprod  35873  dfon3  35880  elfix  35891  dffix2  35893  elfuns  35903  brimg  35925  brapply  35926  brsuccf  35929  funpartlem  35930  funpartfun  35931  brrestrict  35937  dfrecs2  35938  dfrdg4  35939  lineunray  36135  ellines  36140  rmoeqi  36175  reueqi  36177  itgeq12i  36194  finminlem  36306  fneval  36340  neibastop3  36350  eliminable-abelv  36857  bj-inrab  36915  bj-rest10  37076  bj-restpw  37080  bj-restuni  37085  bj-mpomptALT  37107  bj-imdirco  37178  icorempo  37339  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlpssretop  37352  pibt2  37405  wl-ifp-ncond2  37453  wl-df3-3mintru2  37474  wl-2mintru1  37478  rabiun  37587  iundif1  37588  lindsenlbs  37609  poimirlem4  37618  poimirlem25  37639  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  ftc1anc  37695  isbnd2  37777  bndss  37780  heibor1lem  37803  heibor1  37804  isrngohom  37959  isidl  38008  sbccom2lem  38118  anan  38217  eqbrb  38221  eqelb  38223  br1cnvinxp  38245  eldmqsres  38275  idinxpssinxp2  38306  moantr  38346  inxpxrn  38381  dfcoss3  38405  cocossss  38427  ressn2  38433  br1cossinidres  38440  br1cossincnvepres  38441  br1cossxrnidres  38442  br1cossxrncnvepres  38443  refrelcoss2  38455  symrelcoss2  38457  cosscnvssid5  38469  br1cossxrncnvssrres  38499  dfrefrel3  38507  dfcnvrefrel3  38522  cosselcnvrefrels2  38529  cosselcnvrefrels3  38530  cosselcnvrefrels4  38531  cosselcnvrefrels5  38532  dfsymrel3  38541  refsymrel2  38558  refsymrel3  38559  elrefsymrels3  38561  dftrrel3  38569  dfeqvrel2  38581  dfeqvrel3  38582  redundpbi1  38622  refrelredund3  38628  eldmqs1cossres  38651  dffunALTV2  38680  dffunALTV3  38681  dffunALTV4  38682  dffunALTV5  38683  dfdisjALTV  38705  dfdisjALTV2  38706  dfdisjALTV3  38707  dfdisjALTV4  38708  eldisjs3  38716  eldisjs4  38717  disjsuc  38751  prtlem70  38850  prtlem100  38852  prter2  38874  lsateln0  38988  islshpat  39010  lcvnbtwn3  39021  islfl  39053  ishlat1  39345  ishlat2  39346  cvrat4  39437  islvol5  39573  psubspset  39738  snatpsubN  39744  dalawlem13  39877  psubclsetN  39930  isltrn2N  40114  cdlemftr3  40559  dibelval3  41141  dicval2  41173  dicopelval2  41175  dicelval2N  41176  dihglb2  41336  islpolN  41477  lcfls1c  41530  mapdvalc  41623  mapdval4N  41626  mapdordlem1a  41628  aks4d1p8  42075  fimgmcyc  42522  prjsperref  42594  prjspeclsp  42600  elmzpcl  42714  mzpindd  42734  fphpd  42804  pw2f1ocnv  43026  islmodfg  43058  islssfg2  43060  dflim6  43253  onsucf1olem  43259  omge2  43287  tfsconcatlem  43325  tfsconcat0i  43334  rp-isfinite6  43507  minregex  43523  elmapintrab  43565  elinintrab  43566  relintab  43572  dfrtrcl5  43618  fsovrfovd  43998  ntrk1k3eqk13  44039  gneispace3  44122  k0004lem1  44136  pm13.192  44399  opelopab4  44541  ax6e2nd  44548  en3lplem2VD  44833  ax6e2ndVD  44897  ax6e2ndALT  44919  permaxrep  44996  iuneq1i  45079  ssrabf  45108  limcrecl  45627  dvnprodlem2  45945  fourierdlem103  46207  fourierdlem104  46208  4an21  47271  sprvalpwn0  47484  pairreueq  47511  dfvopnbgr2  47853  isubgredg  47866  xpsnopab  48145  sgrp2sgrp  48216  mpomptx2  48323  lindslinindsimp1  48446  lindslinindsimp2  48452  itsclc0b  48761  mo0sn  48804  coxp  48821  isthincd2  49426  thinccic  49460  2arwcatlem1  49584  setc1onsubc  49591  alsconv  49779  aacllem  49790