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  2354  sbel2x  2478  rexcomf  3276  cbvreu  3381  rabeqi  3402  rabrabi  3408  rabrab  3413  ceqsex3v  3483  spc2ed  3543  rexrab  3642  reurab  3647  rmo3f  3680  reuind  3699  rmo3  3827  ssrab  4011  rexun  4136  elin3  4146  inass  4168  rexin  4190  dfun2  4210  inrab2  4257  rabun2  4264  reuun2  4265  undif4  4407  rexdifpr  4603  rexsns  4615  rexdifsn  4739  2ralunsn  4838  iuncom4  4942  iindif1  5017  iunxiun  5039  disjxun  5083  zfrep4  5228  inuni  5291  reusv2lem4  5343  reusv2  5345  otth2  5436  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  copsex2g  5447  copsex4g  5449  vopelopabsb  5484  rabxp  5679  opeliunxp  5698  opeliun2xp  5699  xpundir  5701  xpiundi  5702  xpiundir  5703  brinxp2  5709  copsex2gb  5762  cnvopab  6100  dminss  6117  imainss  6118  difxp  6128  cnvresima  6194  coundi  6211  resco  6214  imaco  6215  rnco  6216  rncoOLD  6217  coiun  6221  coi1  6227  coass  6230  cnvpo  6251  xpco  6253  dfpo2  6260  frpoind  6306  dffun2  6508  fncnv  6571  imadif  6582  mptun  6644  ffrnb  6682  dff1o2  6785  dff1o3  6786  brprcneu  6830  brprcneuALT  6831  fvun2  6932  eqfnfv3  6985  respreima  7018  f1ompt  7063  f1ossf1o  7081  fsn  7088  fmptsng  7123  fmptsnd  7124  tpres  7156  abrexco  7199  imaiun  7200  f1mpt  7216  dff1o6  7230  imaeqsexvOLD  7318  riotarab  7366  oprabidw  7398  oprabid  7399  dfoprab2  7425  oprab4  7453  mpomptx  7480  elpwpwel  7721  elxp4  7873  elxp5  7874  ffoss  7899  f11o  7900  opabex3d  7918  opabex3rd  7919  opabex3  7920  abexssex  7923  elxp7  7977  dfopab2  8005  dfoprab3s  8006  fsplit  8067  frxp  8076  xporderlem  8077  frpoins3xp3g  8091  soseq  8109  suppssov1  8147  suppssov2  8148  suppssfv  8152  brtpos2  8182  tpostpos  8196  tposmpo  8213  dfrecs3  8312  oarec  8497  oeeu  8539  eldifsucnn  8600  naddasslem1  8630  mapsncnv  8841  dfixp  8847  domen  8908  xpsnen  8999  xpcomco  9005  xpassen  9009  sbthlem9  9033  frfi  9195  marypha2lem2  9349  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  12534  elnn0z  12537  fnn0ind  12628  rexuz2  12849  rexrp  12965  elixx3g  13311  elfz2  13468  elfzuzb  13472  fznn  13546  elfz2nn0  13572  fznn0  13573  4fvwrd4  13602  preduz  13604  elfzo2  13616  fzind2  13743  hashgt23el  14386  hashf1lem1  14417  hashf1lem2  14418  fz1isolem  14423  s4f1o  14880  wwlktovfo  14920  fsum2dlem  15732  modfsummod  15757  prodeq1i  15881  sinltx  16156  divalglem10  16371  divalgb  16373  coprmproddvdslem  16631  isprm2  16651  infpn2  16884  prdsle  17425  prdsless  17426  prdsleval  17440  imasleval  17505  xpscf  17529  dfiso2  17739  oppcsect  17745  elhoma  17999  ispos2  18281  lubeldm  18317  glbeldm  18330  tosso  18383  ismgmhm  18664  issubmgm  18670  submgmacs  18685  ismhm  18753  issubm  18771  submacs  18795  issubg  19102  issubg3  19120  gaorb  19282  pmtrrn2  19435  efgcpbllema  19729  efgcpbllemb  19730  frgpuplem  19747  imasabl  19851  subgdmdprd  20011  dprd2d2  20021  omndmul2  20108  dfrhm2  20454  opprnzrb  20498  issubrg  20548  isdomn3  20692  drngprop  20721  drngid2  20729  opprdrng  20741  isabv  20788  isorng  20838  islss  20929  islbs  21071  lsmspsn  21079  isobs  21700  islinds  21789  isassa  21836  aspval2  21878  ltbval  22021  opsrle  22025  opsrtoslem1  22033  fvmptnn04if  22814  ntreq0  23042  restntr  23147  cnnei  23247  hausnei2  23318  cmpcov2  23355  cmpsub  23365  uncmp  23368  cmpfi  23373  llyi  23439  dissnlocfin  23494  iskgen3  23514  1stckgenlem  23518  ptpjpre1  23536  txcnpi  23573  txtube  23605  hausdiag  23610  txlm  23613  txkgen  23617  cfinfil  23858  csdfil  23859  supfil  23860  fin1aufil  23897  elflim2  23929  hauspwpwf1  23952  txflf  23971  isfcls  23974  alexsubALTlem3  24014  alexsubALT  24016  cnextcn  24032  istmd  24039  istgp  24042  tgphaus  24082  qustgplem  24086  istrg  24129  istdrg  24131  istlm  24150  blres  24396  isms2  24415  metrest  24489  metuel2  24530  restmetu  24535  isngp  24561  isnlm  24640  elii1  24902  isclmp  25064  iscvsp  25095  isncvsngp  25116  iscph  25137  cfilucfil3  25287  isbn  25305  limcrcl  25841  ig1pval3  26143  plydivex  26263  ellogdm  26603  cubic  26813  dmarea  26921  vmasum  27179  lgsquadlem1  27343  lgsquadlem2  27344  elno3  27619  lenlts  27716  madeval2  27825  elnnzs  28393  istrkg3ld  28529  legov  28653  ltgov  28665  colinearalg  28979  axeuclid  29032  axcontlem2  29034  axcontlem5  29037  nbgrel  29409  nbupgrres  29433  nbusgredgeu0  29437  nb3grprlem2  29450  nb3grpr2  29452  nb3gr2nb  29453  cplgr3v  29504  finsumvtxdg2ssteplem3  29616  wlkonprop  29725  upgrtrls  29768  upgristrl  29769  wksonproplem  29771  usgr2pth0  29833  wwlksnext  29961  wwlksnextsurj  29968  wwlksnfi  29974  wspthsnwspthsnon  29984  wpthswwlks2on  30032  rusgrnumwwlkl1  30039  erclwwlkref  30090  isclwwlknx  30106  clwwlknwwlksn  30108  clwwlkel  30116  erclwwlknref  30139  clwlknf1oclwwlkn  30154  clwwlknonel  30165  clwwlknon1  30167  clwwlknon2x  30173  clwwlkvbij  30183  iseupthf1o  30272  2pthfrgrrn  30352  fusgr2wsp2nb  30404  numclwwlk1lem2f1  30427  numclwwlkovh  30443  numclwlk2lem2f1o  30449  frgrregord013  30465  avril1  30533  islno  30824  h2hlm  31051  hcau  31255  hhsssh2  31341  dfch2  31478  elcnop  31928  ellnop  31929  elhmop  31944  elcnfn  31953  ellnfn  31954  dmadjss  31958  adjeu  31960  adjval  31961  hhcno  31975  hhcnf  31976  eleigvec  32028  isst  32284  ishst  32285  cvnbtwn3  32359  cvnbtwn4  32360  chirredi  32465  sumdmdii  32486  an52ds  32521  an62ds  32522  an72ds  32523  an82ds  32524  or3di  32528  rexunirn  32561  rmoun  32563  dmrab  32566  difrab2  32567  iunin1f  32627  disjunsn  32664  opeldifid  32669  ofpreima  32738  mpomptxf  32751  fdifsupp  32758  1stpreima  32780  2ndpreima  32781  f1od2  32792  resf1o  32803  maprnin  32804  nndiffz1  32859  ismnt  33043  mgcval  33047  erler  33326  opprnsg  33544  1arithidom  33597  1arithufdlem4  33607  extdgfialglem1  33836  smatrcl  33940  ordtconnlem1  34068  isrrext  34144  sigaex  34254  sigaval  34255  omssubaddlem  34443  omssubadd  34444  eulerpartleme  34507  eulerpartlemt0  34513  eulerpartlemr  34518  eulerpartlemn  34525  probun  34563  ballotlemelo  34632  ballotlem2  34633  ballotlemfc0  34637  ballotlemfcc  34638  reprdifc  34771  bnj248  34843  bnj250  34844  bnj268  34852  bnj312  34855  bnj945  34916  bnj110  35000  bnj849  35067  bnj882  35068  bnj893  35070  bnj916  35075  bnj983  35093  bnj1040  35114  bnj1175  35146  cusgredgex  35304  cusgr3cyclex  35318  erdszelem1  35373  iscvm  35441  elmpst  35718  mpstrcl  35723  dfso3  35902  xpab  35908  coepr  35935  dfdm5  35955  dfrn5  35956  elima4  35958  fv1stcnv  35959  fv2ndcnv  35960  brpprod  36065  dfon3  36072  elfix  36083  dffix2  36085  elfuns  36095  brimg  36117  brapply  36118  lemsuccf  36121  funpartlem  36124  funpartfun  36125  brrestrict  36131  dfrecs2  36132  dfrdg4  36133  lineunray  36329  ellines  36334  rmoeqi  36369  reueqi  36371  itgeq12i  36388  finminlem  36500  fneval  36534  neibastop3  36544  eliminable-abelv  37176  bj-inrab  37234  bj-axseprep  37381  bj-rest10  37400  bj-restpw  37404  bj-restuni  37409  bj-mpomptALT  37431  copsex2gd  37452  bj-imdirco  37504  icorempo  37667  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlpssretop  37680  pibt2  37733  wl-ifp-ncond2  37781  wl-df3-3mintru2  37802  wl-2mintru1  37806  rabiun  37914  iundif1  37915  lindsenlbs  37936  poimirlem4  37945  poimirlem25  37966  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  ftc1anc  38022  isbnd2  38104  bndss  38107  heibor1lem  38130  heibor1  38131  isrngohom  38286  isidl  38335  sbccom2lem  38445  anan  38556  eqbrb  38560  eqelb  38562  br1cnvinxp  38580  eldmqsres  38614  idinxpssinxp2  38645  moantr  38693  inxpxrn  38739  blockadjliftmap  38779  dfcoss3  38825  cocossss  38847  ressn2  38853  br1cossinidres  38860  br1cossincnvepres  38861  br1cossxrnidres  38862  br1cossxrncnvepres  38863  refrelcoss2  38875  symrelcoss2  38877  cosscnvssid5  38889  br1cossxrncnvssrres  38909  dfrefrel3  38917  dfcnvrefrel3  38932  cosselcnvrefrels2  38939  cosselcnvrefrels3  38940  cosselcnvrefrels4  38941  cosselcnvrefrels5  38942  dfsymrel3  38955  refsymrel2  38972  refsymrel3  38973  elrefsymrels3  38975  dftrrel3  38983  dfeqvrel2  38995  dfeqvrel3  38996  redundpbi1  39036  refrelredund3  39042  eldmqs1cossres  39065  dffunALTV2  39094  dffunALTV3  39095  dffunALTV4  39096  dffunALTV5  39097  dfdisjALTV  39119  dfdisjALTV2  39120  dfdisjALTV3  39121  dfdisjALTV4  39122  disjimdmqseq  39130  eldisjs3  39142  eldisjs4  39143  disjsuc  39180  prtlem70  39303  prtlem100  39305  prter2  39327  lsateln0  39441  islshpat  39463  lcvnbtwn3  39474  islfl  39506  ishlat1  39798  ishlat2  39799  cvrat4  39889  islvol5  40025  psubspset  40190  snatpsubN  40196  dalawlem13  40329  psubclsetN  40382  isltrn2N  40566  cdlemftr3  41011  dibelval3  41593  dicval2  41625  dicopelval2  41627  dicelval2N  41628  dihglb2  41788  islpolN  41929  lcfls1c  41982  mapdvalc  42075  mapdval4N  42078  mapdordlem1a  42080  aks4d1p8  42526  fimgmcyc  42979  prjsperref  43039  prjspeclsp  43045  elmzpcl  43158  mzpindd  43178  fphpd  43244  pw2f1ocnv  43465  islmodfg  43497  islssfg2  43499  dflim6  43692  onsucf1olem  43698  omge2  43726  tfsconcatlem  43764  tfsconcat0i  43773  rp-isfinite6  43945  minregex  43961  elmapintrab  44003  elinintrab  44004  relintab  44010  dfrtrcl5  44056  fsovrfovd  44436  ntrk1k3eqk13  44477  gneispace3  44560  k0004lem1  44574  pm13.192  44837  opelopab4  44978  ax6e2nd  44985  en3lplem2VD  45270  ax6e2ndVD  45334  ax6e2ndALT  45356  permaxrep  45433  iuneq1i  45515  ssrabf  45544  limcrecl  46059  dvnprodlem2  46375  fourierdlem103  46637  fourierdlem104  46638  4an21  47718  sprvalpwn0  47943  pairreueq  47970  dfvopnbgr2  48329  isubgredg  48342  xpsnopab  48633  sgrp2sgrp  48704  mpomptx2  48811  lindslinindsimp1  48933  lindslinindsimp2  48939  itsclc0b  49248  mo0sn  49291  coxp  49308  isthincd2  49912  thinccic  49946  2arwcatlem1  50070  setc1onsubc  50077  alsconv  50265  aacllem  50276