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  1122  3ioran  1123  4anpull2OLD  1383  an33rean  1514  an42ds  1520  19.26-3an  1902  sb3an  2115  eeeanv  2382  sbel2x  2506  rexcomf  3304  cbvreu  3408  rabeqi  3429  rabrabi  3435  rabrab  3440  ceqsex3v  3507  spc2ed  3560  rexrab  3659  reurab  3664  rmo3f  3697  reuind  3716  rmo3  3842  ssrab  4025  rexun  4149  elin3  4159  inass  4180  rexin  4203  dfun2  4223  inrab2  4270  rabun2  4277  reuun2  4278  undif4  4427  rexdifpr  4625  rexsns  4637  rexdifsn  4762  2ralunsn  4860  iuncom4  4965  iindif1  5041  iunxiun  5063  disjxun  5107  zfrep4  5254  inuni  5320  reusv2lem4  5372  reusv2  5374  otth2  5465  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  copsex2g  5476  copsex4g  5478  vopelopabsb  5513  rabxp  5709  opeliunxp  5728  opeliun2xp  5729  xpundir  5731  xpiundi  5732  xpiundir  5733  brinxp2  5739  copsex2gb  5793  cnvopab  6137  dminss  6150  imainss  6151  difxp  6161  cnvresima  6231  coundi  6248  resco  6251  imaco  6252  rnco  6253  rncoOLD  6254  coiun  6258  coi1  6264  coass  6267  cnvpo  6288  xpco  6290  dfpo2  6297  frpoind  6343  dffun2  6546  fncnv  6609  imadif  6620  mptun  6681  ffrnb  6720  dff1o2  6826  dff1o3  6827  brprcneu  6871  brprcneuALT  6872  fvun2  6973  eqfnfv3  7027  respreima  7061  f1ompt  7106  f1ossf1o  7124  fsn  7131  fmptsng  7166  fmptsnd  7167  tpres  7199  abrexco  7242  imaiun  7243  f1mpt  7259  dff1o6  7273  imaeqsexvOLD  7361  riotarab  7409  oprabidw  7441  oprabid  7442  dfoprab2  7468  oprab4  7496  mpomptx  7523  elpwpwel  7762  elxp4  7915  elxp5  7916  ffoss  7939  f11o  7940  opabex3d  7958  opabex3rd  7959  opabex3  7960  abexssex  7963  elxp7  8017  dfopab2  8045  dfoprab3s  8046  fsplit  8108  frxp  8118  xporderlem  8119  frpoins3xp3g  8133  soseq  8151  suppssov1  8189  suppssov2  8190  suppssfv  8194  brtpos2  8224  tpostpos  8238  tposmpo  8255  dfrecs3  8355  oarec  8543  oeeu  8585  eldifsucnn  8646  naddasslem1  8677  mapsncnv  8887  dfixp  8893  domen  8954  xpsnen  9045  xpcomco  9051  xpassen  9055  sbthlem9  9079  frfi  9241  marypha2lem2  9392  brttrcl2  9679  epfrs  9696  tcsni  9706  frind  9718  cp  9873  dfac5lem1  10103  dfac5lem2  10104  dfac5lem5  10107  kmlem3  10132  dfackm  10146  cfval2  10239  cflim3  10241  cfss  10244  cfslb  10245  zfcndrep  10594  eltsk2g  10731  ltexpi  10882  recmulnq  10944  ltexprlem4  11019  addsrpr  11055  mulsrpr  11056  addcnsr  11115  mulcnsr  11116  ltresr  11120  axrrecex  11143  elnnz  12596  elnn0z  12599  fnn0ind  12690  rexuz2  12918  rexrp  13034  elixx3g  13380  elfz2  13537  elfzuzb  13541  fznn  13616  elfz2nn0  13642  fznn0  13643  4fvwrd4  13672  preduz  13674  elfzo2  13686  fzind2  13813  hashgt23el  14457  hashf1lem1  14488  hashf1lem2  14489  fz1isolem  14494  s4f1o  14951  wwlktovfo  14991  fsum2dlem  15817  modfsummod  15842  prodeq1i  15966  sinltx  16240  divalglem10  16455  divalgb  16457  coprmproddvdslem  16715  isprm2  16735  infpn2  16968  prdsle  17510  prdsless  17511  prdsleval  17525  imasleval  17590  xpscf  17614  dfiso2  17824  oppcsect  17830  elhoma  18084  ispos2  18366  lubeldm  18402  glbeldm  18415  tosso  18468  ismgmhm  18749  issubmgm  18755  submgmacs  18770  ismhm  18838  issubm  18856  submacs  18881  issubg  19187  issubg3  19206  gaorb  19372  pmtrrn2  19525  efgcpbllema  19819  efgcpbllemb  19820  frgpuplem  19837  imasabl  19941  subgdmdprd  20101  dprd2d2  20111  omndmul2  20198  dfrhm2  20552  isrhm0  20554  opprnzrb  20619  issubrg  20670  isdomn3  20813  drngprop  20844  drngid2  20856  opprdrng  20867  isabv  20914  isorng  20964  islss  21055  islbs  21197  lsmspsn  21205  isobs  21870  islinds  21959  isassa  22006  aspval2  22048  ltbval  22194  opsrle  22198  opsrtoslem1  22206  fvmptnn04if  23006  ntreq0  23234  restntr  23339  cnnei  23439  hausnei2  23510  cmpcov2  23547  cmpsub  23557  uncmp  23560  cmpfi  23565  llyi  23631  dissnlocfin  23686  iskgen3  23706  1stckgenlem  23710  ptpjpre1  23728  txcnpi  23765  txtube  23797  hausdiag  23802  txlm  23805  txkgen  23809  cfinfil  24050  csdfil  24051  supfil  24052  fin1aufil  24089  elflim2  24121  hauspwpwf1  24144  txflf  24163  isfcls  24166  alexsubALTlem3  24206  alexsubALT  24208  cnextcn  24224  istmd  24231  istgp  24234  tgphaus  24274  qustgplem  24278  istrg  24321  istdrg  24323  istlm  24342  blres  24588  isms2  24607  metrest  24681  metuel2  24722  restmetu  24727  isngp  24753  isnlm  24832  elii1  25094  isclmp  25256  iscvsp  25287  isncvsngp  25308  iscph  25329  cfilucfil3  25479  isbn  25497  limcrcl  26033  ig1pval3  26335  plydivex  26458  ellogdm  26804  cubic  27014  dmarea  27122  vmasum  27380  lgsquadlem1  27544  lgsquadlem2  27545  elno3  27819  lenlts  27916  madeval2  28026  elnnzs  28594  istrkg3ld  28730  legov  28854  ltgov  28866  colinearalg  29260  axeuclid  29313  axcontlem2  29315  axcontlem5  29318  nbgrel  29690  nbupgrres  29714  nbusgredgeu0  29718  nb3grprlem2  29731  nb3grpr2  29733  nb3gr2nb  29734  cplgr3v  29785  finsumvtxdg2ssteplem3  29897  wlkonprop  30006  upgrtrls  30049  upgristrl  30050  wksonproplem  30052  usgr2pth0  30114  wwlksnext  30242  wwlksnextsurj  30249  wwlksnfi  30255  wspthsnwspthsnon  30265  wpthswwlks2on  30313  rusgrnumwwlkl1  30320  erclwwlkref  30371  isclwwlknx  30387  clwwlknwwlksn  30389  clwwlkel  30397  erclwwlknref  30420  clwlknf1oclwwlkn  30435  clwwlknonel  30446  clwwlknon1  30448  clwwlknon2x  30454  clwwlkvbij  30464  iseupthf1o  30553  2pthfrgrrn  30633  fusgr2wsp2nb  30685  numclwwlk1lem2f1  30708  numclwwlkovh  30724  numclwlk2lem2f1o  30730  frgrregord013  30746  avril1  30814  islno  31105  h2hlm  31332  hcau  31536  hhsssh2  31622  dfch2  31759  elcnop  32209  ellnop  32210  elhmop  32225  elcnfn  32234  ellnfn  32235  dmadjss  32239  adjeu  32241  adjval  32242  hhcno  32256  hhcnf  32257  eleigvec  32309  isst  32565  ishst  32566  cvnbtwn3  32640  cvnbtwn4  32641  chirredi  32746  sumdmdii  32767  an52ds  32802  an62ds  32803  an72ds  32804  an82ds  32805  or3di  32807  rexunirn  32838  rmoun  32840  dmrab  32843  difrab2  32844  iunin1f  32902  disjunsn  32939  opeldifid  32944  ofpreima  33010  mpomptxf  33023  fdifsupp  33030  1stpreima  33052  2ndpreima  33053  f1od2  33064  resf1o  33075  maprnin  33076  nndiffz1  33131  ismnt  33303  mgcval  33307  erler  33585  opprnsg  33766  1arithidom  33827  1arithufdlem4  33837  extdgfialglem1  34082  smatrcl  34186  ordtconnlem1  34314  isrrext  34390  sigaex  34500  sigaval  34501  omssubaddlem  34689  omssubadd  34690  eulerpartleme  34753  eulerpartlemt0  34759  eulerpartlemr  34764  eulerpartlemn  34771  probun  34809  ballotlemelo  34878  ballotlem2  34879  ballotlemfc0  34883  ballotlemfcc  34884  reprdifc  35014  bnj248  35089  bnj250  35090  bnj268  35098  bnj312  35101  bnj945  35162  bnj110  35246  bnj849  35313  bnj882  35314  bnj893  35316  bnj916  35321  bnj983  35339  bnj1040  35360  bnj1175  35392  cusgredgex  35614  cusgr3cyclex  35628  erdszelem1  35683  iscvm  35751  elmpst  36028  mpstrcl  36033  dfso3  36212  xpab  36218  coepr  36245  dfdm5  36265  dfrn5  36266  elima4  36268  fv1stcnv  36269  fv2ndcnv  36270  brpprod  36375  dfon3  36382  elfix  36393  dffix2  36395  elfuns  36405  brimg  36427  brapply  36428  lemsuccf  36431  funpartlem  36434  funpartfun  36435  brrestrict  36441  dfrecs2  36442  dfrdg4  36443  lineunray  36639  ellines  36644  rmoeqi  36699  reueqi  36701  itgeq12i  36718  finminlem  36829  fneval  36863  neibastop3  36873  eliminable-abelv  37504  bj-inrab  37563  bj-axseprep  37711  bj-rest10  37730  bj-restpw  37734  bj-restuni  37739  bj-mpomptALT  37761  copsex2gd  37782  bj-imdirco  37834  icorempo  37997  isbasisrelowllem1  38001  isbasisrelowllem2  38002  relowlpssretop  38010  pibt2  38063  wl-ifp-ncond2  38111  wl-df3-3mintru2  38132  wl-2mintru1  38136  rabiun  38244  iundif1  38245  lindsenlbs  38266  poimirlem4  38275  poimirlem25  38296  poimirlem26  38297  poimirlem29  38300  poimirlem30  38301  ismblfin  38312  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  itg2addnclem2  38323  itg2addnclem3  38324  itg2addnc  38325  ftc1anc  38352  isbnd2  38434  bndss  38437  heibor1lem  38460  heibor1  38461  isrngohom  38616  isidl  38665  sbccom2lem  38773  anan  38884  eqbrb  38888  eqelb  38890  br1cnvinxp  38908  eldmqsres  38942  idinxpssinxp2  38973  moantr  39021  inxpxrn  39067  blockadjliftmap  39107  dfcoss3  39153  cocossss  39175  ressn2  39181  br1cossinidres  39188  br1cossincnvepres  39189  br1cossxrnidres  39190  br1cossxrncnvepres  39191  refrelcoss2  39203  symrelcoss2  39205  cosscnvssid5  39217  br1cossxrncnvssrres  39237  dfrefrel3  39245  dfcnvrefrel3  39260  cosselcnvrefrels2  39267  cosselcnvrefrels3  39268  cosselcnvrefrels4  39269  cosselcnvrefrels5  39270  dfsymrel3  39283  refsymrel2  39300  refsymrel3  39301  elrefsymrels3  39303  dftrrel3  39311  dfeqvrel2  39323  dfeqvrel3  39324  redundpbi1  39364  refrelredund3  39370  eldmqs1cossres  39393  dffunALTV2  39422  dffunALTV3  39423  dffunALTV4  39424  dffunALTV5  39425  dfdisjALTV  39447  dfdisjALTV2  39448  dfdisjALTV3  39449  dfdisjALTV4  39450  disjimdmqseq  39458  eldisjs3  39470  eldisjs4  39471  disjsuc  39508  prtlem70  39631  prtlem100  39633  prter2  39655  lsateln0  39769  islshpat  39791  lcvnbtwn3  39802  islfl  39834  ishlat1  40126  ishlat2  40127  cvrat4  40217  islvol5  40353  psubspset  40518  snatpsubN  40524  dalawlem13  40657  psubclsetN  40710  isltrn2N  40894  cdlemftr3  41339  dibelval3  41921  dicval2  41953  dicopelval2  41955  dicelval2N  41956  dihglb2  42116  islpolN  42257  lcfls1c  42310  mapdvalc  42403  mapdval4N  42406  mapdordlem1a  42408  aks4d1p8  42854  fimgmcyc  43302  prjsperref  43338  prjspeclsp  43344  elmzpcl  43457  mzpindd  43477  fphpd  43543  pw2f1ocnv  43764  islmodfg  43796  islssfg2  43798  dflim6  43991  onsucf1olem  43997  omge2  44025  tfsconcatlem  44063  tfsconcat0i  44072  rp-isfinite6  44244  minregex  44260  elmapintrab  44302  elinintrab  44303  relintab  44309  dfrtrcl5  44355  fsovrfovd  44735  ntrk1k3eqk13  44776  gneispace3  44859  k0004lem1  44873  pm13.192  45120  opelopab4  45260  ax6e2nd  45267  en3lplem2VD  45552  ax6e2ndVD  45616  ax6e2ndALT  45638  permaxrep  45715  iuneq1i  45804  ssrabf  45832  limcrecl  46345  dvnprodlem2  46661  fourierdlem103  46923  fourierdlem104  46924  4an21  48007  sprvalpwn0  48232  pairreueq  48259  dfvopnbgr2  48618  isubgredg  48631  xpsnopab  48922  sgrp2sgrp  48993  mpomptx2  49115  lindslinindsimp1  49237  lindslinindsimp2  49243  itsclc0b  49552  mo0sn  49594  coxp  49611  isthincd2  50215  thinccic  50249  2arwcatlem1  50373  setc1onsubc  50380  alsanmo  50588  ralsanmo  50589  alsralrex  50590  aacllem  50621