Theorem anbi1i 635

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi2ci  636  bianbi  638  anandi  688  3an4anass  1120  3ioran  1121  4anpull2OLD  1381  an33rean  1511  an42ds  1517  19.26-3an  1899  sb3an  2121  eeeanv  2388  sbel2x  2512  rexcomf  3310  cbvreu  3415  rabeqi  3436  rabrabi  3442  rabrab  3447  ceqsex3v  3515  spc2ed  3569  rexrab  3668  reurab  3673  rmo3f  3706  reuind  3725  rmo3  3851  ssrab  4033  rexun  4157  elin3  4167  inass  4188  rexin  4211  dfun2  4231  inrab2  4278  rabun2  4285  reuun2  4286  undif4  4433  rexdifpr  4630  rexsns  4642  rexdifsn  4766  2ralunsn  4864  iuncom4  4969  iindif1  5045  iunxiun  5067  disjxun  5111  zfrep4  5258  inuni  5321  reusv2lem4  5373  reusv2  5375  otth2  5466  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  copsex2g  5477  copsex4g  5479  vopelopabsb  5514  rabxp  5710  opeliunxp  5729  opeliun2xp  5730  xpundir  5732  xpiundi  5733  xpiundir  5734  brinxp2  5740  copsex2gb  5794  cnvopab  6138  dminss  6151  imainss  6152  difxp  6162  cnvresima  6232  coundi  6249  resco  6252  imaco  6253  rnco  6254  rncoOLD  6255  coiun  6259  coi1  6265  coass  6268  cnvpo  6289  xpco  6291  dfpo2  6298  frpoind  6344  dffun2  6547  fncnv  6610  imadif  6621  mptun  6682  ffrnb  6721  dff1o2  6827  dff1o3  6828  brprcneu  6872  brprcneuALT  6873  fvun2  6974  eqfnfv3  7028  respreima  7062  f1ompt  7107  f1ossf1o  7125  fsn  7132  fmptsng  7167  fmptsnd  7168  tpres  7200  abrexco  7243  imaiun  7244  f1mpt  7260  dff1o6  7274  imaeqsexvOLD  7362  riotarab  7410  oprabidw  7442  oprabid  7443  dfoprab2  7469  oprab4  7497  mpomptx  7524  elpwpwel  7765  elxp4  7918  elxp5  7919  ffoss  7942  f11o  7943  opabex3d  7961  opabex3rd  7962  opabex3  7963  abexssex  7966  elxp7  8020  dfopab2  8048  dfoprab3s  8049  fsplit  8111  frxp  8121  xporderlem  8122  frpoins3xp3g  8136  soseq  8154  suppssov1  8192  suppssov2  8193  suppssfv  8197  brtpos2  8227  tpostpos  8241  tposmpo  8258  dfrecs3  8358  oarec  8546  oeeu  8588  eldifsucnn  8649  naddasslem1  8680  mapsncnv  8890  dfixp  8896  domen  8957  xpsnen  9048  xpcomco  9054  xpassen  9058  sbthlem9  9082  frfi  9244  marypha2lem2  9395  brttrcl2  9682  epfrs  9699  tcsni  9709  frind  9721  cp  9876  dfac5lem1  10106  dfac5lem2  10107  dfac5lem5  10110  kmlem3  10135  dfackm  10149  cfval2  10243  cflim3  10245  cfss  10248  cfslb  10249  zfcndrep  10598  eltsk2g  10735  ltexpi  10886  recmulnq  10948  ltexprlem4  11023  addsrpr  11059  mulsrpr  11060  addcnsr  11119  mulcnsr  11120  ltresr  11124  axrrecex  11147  elnnz  12600  elnn0z  12603  fnn0ind  12694  rexuz2  12922  rexrp  13038  elixx3g  13384  elfz2  13541  elfzuzb  13545  fznn  13619  elfz2nn0  13645  fznn0  13646  4fvwrd4  13675  preduz  13677  elfzo2  13689  fzind2  13816  hashgt23el  14460  hashf1lem1  14491  hashf1lem2  14492  fz1isolem  14497  s4f1o  14954  wwlktovfo  14994  fsum2dlem  15820  modfsummod  15845  prodeq1i  15969  sinltx  16244  divalglem10  16459  divalgb  16461  coprmproddvdslem  16719  isprm2  16739  infpn2  16972  prdsle  17514  prdsless  17515  prdsleval  17529  imasleval  17594  xpscf  17618  dfiso2  17828  oppcsect  17834  elhoma  18088  ispos2  18370  lubeldm  18406  glbeldm  18419  tosso  18472  ismgmhm  18753  issubmgm  18759  submgmacs  18774  ismhm  18842  issubm  18860  submacs  18885  issubg  19191  issubg3  19210  gaorb  19376  pmtrrn2  19529  efgcpbllema  19823  efgcpbllemb  19824  frgpuplem  19841  imasabl  19945  subgdmdprd  20105  dprd2d2  20115  omndmul2  20202  dfrhm2  20555  opprnzrb  20604  issubrg  20655  isdomn3  20798  drngprop  20827  drngid2  20834  opprdrng  20845  isabv  20891  isorng  20941  islss  21032  islbs  21174  lsmspsn  21182  isobs  21838  islinds  21927  isassa  21974  aspval2  22016  ltbval  22162  opsrle  22166  opsrtoslem1  22174  fvmptnn04if  22974  ntreq0  23202  restntr  23307  cnnei  23407  hausnei2  23478  cmpcov2  23515  cmpsub  23525  uncmp  23528  cmpfi  23533  llyi  23599  dissnlocfin  23654  iskgen3  23674  1stckgenlem  23678  ptpjpre1  23696  txcnpi  23733  txtube  23765  hausdiag  23770  txlm  23773  txkgen  23777  cfinfil  24018  csdfil  24019  supfil  24020  fin1aufil  24057  elflim2  24089  hauspwpwf1  24112  txflf  24131  isfcls  24134  alexsubALTlem3  24174  alexsubALT  24176  cnextcn  24192  istmd  24199  istgp  24202  tgphaus  24242  qustgplem  24246  istrg  24289  istdrg  24291  istlm  24310  blres  24556  isms2  24575  metrest  24649  metuel2  24690  restmetu  24695  isngp  24721  isnlm  24800  elii1  25062  isclmp  25224  iscvsp  25255  isncvsngp  25276  iscph  25297  cfilucfil3  25447  isbn  25465  limcrcl  26001  ig1pval3  26303  plydivex  26426  ellogdm  26769  cubic  26979  dmarea  27087  vmasum  27345  lgsquadlem1  27509  lgsquadlem2  27510  elno3  27784  lenlts  27881  madeval2  27991  elnnzs  28559  istrkg3ld  28695  legov  28819  ltgov  28831  colinearalg  29200  axeuclid  29253  axcontlem2  29255  axcontlem5  29258  nbgrel  29630  nbupgrres  29654  nbusgredgeu0  29658  nb3grprlem2  29671  nb3grpr2  29673  nb3gr2nb  29674  cplgr3v  29725  finsumvtxdg2ssteplem3  29837  wlkonprop  29946  upgrtrls  29989  upgristrl  29990  wksonproplem  29992  usgr2pth0  30054  wwlksnext  30182  wwlksnextsurj  30189  wwlksnfi  30195  wspthsnwspthsnon  30205  wpthswwlks2on  30253  rusgrnumwwlkl1  30260  erclwwlkref  30311  isclwwlknx  30327  clwwlknwwlksn  30329  clwwlkel  30337  erclwwlknref  30360  clwlknf1oclwwlkn  30375  clwwlknonel  30386  clwwlknon1  30388  clwwlknon2x  30394  clwwlkvbij  30404  iseupthf1o  30493  2pthfrgrrn  30573  fusgr2wsp2nb  30625  numclwwlk1lem2f1  30648  numclwwlkovh  30664  numclwlk2lem2f1o  30670  frgrregord013  30686  avril1  30754  islno  31045  h2hlm  31272  hcau  31476  hhsssh2  31562  dfch2  31699  elcnop  32149  ellnop  32150  elhmop  32165  elcnfn  32174  ellnfn  32175  dmadjss  32179  adjeu  32181  adjval  32182  hhcno  32196  hhcnf  32197  eleigvec  32249  isst  32505  ishst  32506  cvnbtwn3  32580  cvnbtwn4  32581  chirredi  32686  sumdmdii  32707  an52ds  32742  an62ds  32743  an72ds  32744  an82ds  32745  or3di  32747  rexunirn  32778  rmoun  32780  dmrab  32783  difrab2  32784  iunin1f  32842  disjunsn  32879  opeldifid  32884  ofpreima  32950  mpomptxf  32963  fdifsupp  32970  1stpreima  32992  2ndpreima  32993  f1od2  33004  resf1o  33015  maprnin  33016  nndiffz1  33071  ismnt  33243  mgcval  33247  erler  33525  opprnsg  33710  1arithidom  33771  1arithufdlem4  33781  extdgfialglem1  34026  smatrcl  34130  ordtconnlem1  34258  isrrext  34334  sigaex  34444  sigaval  34445  omssubaddlem  34633  omssubadd  34634  eulerpartleme  34697  eulerpartlemt0  34703  eulerpartlemr  34708  eulerpartlemn  34715  probun  34753  ballotlemelo  34822  ballotlem2  34823  ballotlemfc0  34827  ballotlemfcc  34828  reprdifc  34958  bnj248  35033  bnj250  35034  bnj268  35042  bnj312  35045  bnj945  35106  bnj110  35190  bnj849  35257  bnj882  35258  bnj893  35260  bnj916  35265  bnj983  35283  bnj1040  35304  bnj1175  35336  cusgredgex  35512  cusgr3cyclex  35526  erdszelem1  35581  iscvm  35649  elmpst  35926  mpstrcl  35931  dfso3  36110  xpab  36116  coepr  36143  dfdm5  36163  dfrn5  36164  elima4  36166  fv1stcnv  36167  fv2ndcnv  36168  brpprod  36273  dfon3  36280  elfix  36291  dffix2  36293  elfuns  36303  brimg  36325  brapply  36326  lemsuccf  36329  funpartlem  36332  funpartfun  36333  brrestrict  36339  dfrecs2  36340  dfrdg4  36341  lineunray  36537  ellines  36542  rmoeqi  36587  reueqi  36589  itgeq12i  36606  finminlem  36717  fneval  36751  neibastop3  36761  eliminable-abelv  37392  bj-inrab  37450  bj-axseprep  37598  bj-rest10  37617  bj-restpw  37621  bj-restuni  37626  bj-mpomptALT  37648  copsex2gd  37669  bj-imdirco  37721  icorempo  37884  isbasisrelowllem1  37888  isbasisrelowllem2  37889  relowlpssretop  37897  pibt2  37950  wl-ifp-ncond2  37998  wl-df3-3mintru2  38019  wl-2mintru1  38023  rabiun  38131  iundif1  38132  lindsenlbs  38153  poimirlem4  38162  poimirlem25  38183  poimirlem26  38184  poimirlem29  38187  poimirlem30  38188  ismblfin  38199  ovoliunnfl  38200  voliunnfl  38202  volsupnfl  38203  itg2addnclem2  38210  itg2addnclem3  38211  itg2addnc  38212  ftc1anc  38239  isbnd2  38321  bndss  38324  heibor1lem  38347  heibor1  38348  isrngohom  38503  isidl  38552  sbccom2lem  38662  anan  38773  eqbrb  38777  eqelb  38779  br1cnvinxp  38797  eldmqsres  38831  idinxpssinxp2  38862  moantr  38910  inxpxrn  38956  blockadjliftmap  38996  dfcoss3  39042  cocossss  39064  ressn2  39070  br1cossinidres  39077  br1cossincnvepres  39078  br1cossxrnidres  39079  br1cossxrncnvepres  39080  refrelcoss2  39092  symrelcoss2  39094  cosscnvssid5  39106  br1cossxrncnvssrres  39126  dfrefrel3  39134  dfcnvrefrel3  39149  cosselcnvrefrels2  39156  cosselcnvrefrels3  39157  cosselcnvrefrels4  39158  cosselcnvrefrels5  39159  dfsymrel3  39172  refsymrel2  39189  refsymrel3  39190  elrefsymrels3  39192  dftrrel3  39200  dfeqvrel2  39212  dfeqvrel3  39213  redundpbi1  39253  refrelredund3  39259  eldmqs1cossres  39282  dffunALTV2  39311  dffunALTV3  39312  dffunALTV4  39313  dffunALTV5  39314  dfdisjALTV  39336  dfdisjALTV2  39337  dfdisjALTV3  39338  dfdisjALTV4  39339  disjimdmqseq  39347  eldisjs3  39359  eldisjs4  39360  disjsuc  39397  prtlem70  39520  prtlem100  39522  prter2  39544  lsateln0  39658  islshpat  39680  lcvnbtwn3  39691  islfl  39723  ishlat1  40015  ishlat2  40016  cvrat4  40106  islvol5  40242  psubspset  40407  snatpsubN  40413  dalawlem13  40546  psubclsetN  40599  isltrn2N  40783  cdlemftr3  41228  dibelval3  41810  dicval2  41842  dicopelval2  41844  dicelval2N  41845  dihglb2  42005  islpolN  42146  lcfls1c  42199  mapdvalc  42292  mapdval4N  42295  mapdordlem1a  42297  aks4d1p8  42743  fimgmcyc  43193  prjsperref  43229  prjspeclsp  43235  elmzpcl  43348  mzpindd  43368  fphpd  43434  pw2f1ocnv  43655  islmodfg  43687  islssfg2  43689  dflim6  43882  onsucf1olem  43888  omge2  43916  tfsconcatlem  43954  tfsconcat0i  43963  rp-isfinite6  44135  minregex  44151  elmapintrab  44193  elinintrab  44194  relintab  44200  dfrtrcl5  44246  fsovrfovd  44626  ntrk1k3eqk13  44667  gneispace3  44750  k0004lem1  44764  pm13.192  45011  opelopab4  45151  ax6e2nd  45158  en3lplem2VD  45443  ax6e2ndVD  45507  ax6e2ndALT  45529  permaxrep  45606  iuneq1i  45695  ssrabf  45723  limcrecl  46236  dvnprodlem2  46552  fourierdlem103  46814  fourierdlem104  46815  4an21  47895  sprvalpwn0  48120  pairreueq  48147  dfvopnbgr2  48506  isubgredg  48519  xpsnopab  48810  sgrp2sgrp  48881  mpomptx2  48999  lindslinindsimp1  49121  lindslinindsimp2  49127  itsclc0b  49436  mo0sn  49478  coxp  49495  isthincd2  50099  thinccic  50133  2arwcatlem1  50257  setc1onsubc  50264  aacllem  50474