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  an6  1444  an33rean  1482  19.26-3an  1869  sb3an  2078  eeeanv  2350  sbel2x  2476  rexcomf  3300  cbvreuwOLD  3412  cbvreu  3424  rabeqi  3446  rabrabi  3452  rabrab  3457  ceqsex3v  3536  spc2ed  3600  rexabOLD  3703  rexrab  3704  reurab  3709  rmo3f  3742  reuind  3761  rmo3  3897  ssrab  4082  rexun  4205  elin3  4215  inass  4235  rexin  4255  dfun2  4275  inrab2  4322  rabun2  4329  reuun2  4330  undif4  4472  rexdifpr  4663  rexsns  4675  rexdifsn  4798  2ralunsn  4899  iuncom4  5004  iindif1  5079  iunxiun  5101  disjxun  5145  zfrep4  5298  inuni  5355  reusv2lem4  5406  reusv2  5408  otth2  5493  copsexgw  5500  copsexg  5501  copsex2g  5503  copsex4g  5504  vopelopabsb  5538  rabxp  5736  opeliunxp  5755  xpundir  5757  xpiundi  5758  xpiundir  5759  brinxp2  5765  copsex2gb  5818  cnvopab  6159  dminss  6174  imainss  6175  difxp  6185  cnvresima  6251  coundi  6268  resco  6271  imaco  6272  rnco  6273  coiun  6277  coi1  6283  coass  6286  cnvpo  6308  xpco  6310  dfpo2  6317  frpoind  6364  wfiOLD  6373  dffun2  6572  dffun2OLD  6573  dffun2OLDOLD  6574  fncnv  6640  imadif  6651  mptun  6714  ffrnb  6750  dff1o2  6853  dff1o3  6854  brprcneu  6896  brprcneuALT  6897  fvun2  7000  eqfnfv3  7052  respreima  7085  f1ompt  7130  f1ossf1o  7147  fsn  7154  fmptsng  7187  fmptsnd  7188  tpres  7220  abrexco  7263  imaiun  7264  f1mpt  7280  dff1o6  7294  imaeqsexvOLD  7382  riotarab  7429  oprabidw  7461  oprabid  7462  dfoprab2  7490  oprab4  7518  mpomptx  7545  elpwpwel  7785  elxp4  7944  elxp5  7945  ffoss  7968  f11o  7969  opabex3d  7988  opabex3rd  7989  opabex3  7990  abexssex  7993  elxp7  8047  dfopab2  8075  dfoprab3s  8076  fsplit  8140  frxp  8149  xporderlem  8150  frpoins3xp3g  8164  soseq  8182  suppssov1  8220  suppssov2  8221  suppssfv  8225  brtpos2  8255  tpostpos  8269  tposmpo  8286  wfrfunOLD  8357  dfrecs3  8410  dfrecs3OLD  8411  oarec  8598  oeeu  8639  eldifsucnn  8700  naddasslem1  8730  mapsncnv  8931  dfixp  8937  domen  9000  xpsnen  9093  xpcomco  9100  xpassen  9104  sbthlem9  9129  frfi  9318  marypha2lem2  9473  brttrcl2  9751  epfrs  9768  tcsni  9780  frind  9787  cp  9928  dfac5lem1  10160  dfac5lem2  10161  dfac5lem5  10164  kmlem3  10190  dfackm  10204  cfval2  10297  cflim3  10299  cfss  10302  cfslb  10303  zfcndrep  10651  eltsk2g  10788  ltexpi  10939  recmulnq  11001  ltexprlem4  11076  addsrpr  11112  mulsrpr  11113  addcnsr  11172  mulcnsr  11173  ltresr  11177  axrrecex  11200  elnnz  12620  elnn0z  12623  fnn0ind  12714  rexuz2  12938  rexrp  13053  elixx3g  13396  elfz2  13550  elfzuzb  13554  fznn  13628  elfz2nn0  13654  fznn0  13655  4fvwrd4  13684  preduz  13686  elfzo2  13698  fzind2  13820  hashgt23el  14459  hashf1lem1  14490  hashf1lem2  14491  fz1isolem  14496  s4f1o  14953  wwlktovfo  14993  fsum2dlem  15802  modfsummod  15826  prodeq1i  15948  sinltx  16221  divalglem10  16435  divalgb  16437  coprmproddvdslem  16695  isprm2  16715  infpn2  16946  prdsle  17508  prdsless  17509  prdsleval  17523  imasleval  17587  xpscf  17611  dfiso2  17819  oppcsect  17825  elhoma  18085  ispos2  18372  lubeldm  18410  glbeldm  18423  tosso  18476  ismgmhm  18721  issubmgm  18727  submgmacs  18742  ismhm  18810  issubm  18828  submacs  18852  issubg  19156  issubg3  19174  gaorb  19337  pmtrrn2  19492  efgcpbllema  19786  efgcpbllemb  19787  frgpuplem  19804  imasabl  19908  subgdmdprd  20068  dprd2d2  20078  dfrhm2  20490  opprnzrb  20537  issubrg  20587  isdomn3  20731  drngprop  20760  drngid2  20768  opprdrng  20780  isabv  20828  islss  20949  islbs  21092  lsmspsn  21100  isobs  21757  islinds  21846  isassa  21893  aspval2  21935  ltbval  22078  opsrle  22082  opsrtoslem1  22096  fvmptnn04if  22870  ntreq0  23100  restntr  23205  cnnei  23305  hausnei2  23376  cmpcov2  23413  cmpsub  23423  uncmp  23426  cmpfi  23431  llyi  23497  dissnlocfin  23552  iskgen3  23572  1stckgenlem  23576  ptpjpre1  23594  txcnpi  23631  txtube  23663  hausdiag  23668  txlm  23671  txkgen  23675  cfinfil  23916  csdfil  23917  supfil  23918  fin1aufil  23955  elflim2  23987  hauspwpwf1  24010  txflf  24029  isfcls  24032  alexsubALTlem3  24072  alexsubALT  24074  cnextcn  24090  istmd  24097  istgp  24100  tgphaus  24140  qustgplem  24144  istrg  24187  istdrg  24189  istlm  24208  blres  24456  isms2  24475  metrest  24552  metuel2  24593  restmetu  24598  isngp  24624  isnlm  24711  elii1  24977  isclmp  25143  iscvsp  25174  isncvsngp  25196  iscph  25217  cfilucfil3  25367  isbn  25385  limcrcl  25923  ig1pval3  26231  plydivex  26353  ellogdm  26695  cubic  26906  dmarea  27014  vmasum  27274  lgsquadlem1  27438  lgsquadlem2  27439  elno3  27714  slenlt  27811  madeval2  27906  elnnzs  28401  istrkg3ld  28483  legov  28607  ltgov  28619  colinearalg  28939  axeuclid  28992  axcontlem2  28994  axcontlem5  28997  nbgrel  29371  nbupgrres  29395  nbusgredgeu0  29399  nb3grprlem2  29412  nb3grpr2  29414  nb3gr2nb  29415  cplgr3v  29466  finsumvtxdg2ssteplem3  29579  wlkonprop  29690  upgrtrls  29733  upgristrl  29734  wksonproplem  29736  wksonproplemOLD  29737  usgr2pth0  29797  wwlksnext  29922  wwlksnextsurj  29929  wwlksnfi  29935  wspthsnwspthsnon  29945  wpthswwlks2on  29990  rusgrnumwwlkl1  29997  erclwwlkref  30048  isclwwlknx  30064  clwwlknwwlksn  30066  clwwlkel  30074  erclwwlknref  30097  clwlknf1oclwwlkn  30112  clwwlknonel  30123  clwwlknon1  30125  clwwlknon2x  30131  clwwlkvbij  30141  iseupthf1o  30230  2pthfrgrrn  30310  fusgr2wsp2nb  30362  numclwwlk1lem2f1  30385  numclwwlkovh  30401  numclwlk2lem2f1o  30407  frgrregord013  30423  avril1  30491  islno  30781  h2hlm  31008  hcau  31212  hhsssh2  31298  dfch2  31435  elcnop  31885  ellnop  31886  elhmop  31901  elcnfn  31910  ellnfn  31911  dmadjss  31915  adjeu  31917  adjval  31918  hhcno  31932  hhcnf  31933  eleigvec  31985  isst  32241  ishst  32242  cvnbtwn3  32316  cvnbtwn4  32317  chirredi  32422  sumdmdii  32443  an42ds  32478  an52ds  32479  an62ds  32480  an72ds  32481  an82ds  32482  or3di  32487  rexunirn  32519  rmoun  32521  dmrab  32524  difrab2  32525  iunin1f  32577  disjunsn  32613  opeldifid  32618  ofpreima  32681  mpomptxf  32693  fdifsupp  32699  1stpreima  32721  2ndpreima  32722  f1od2  32738  resf1o  32747  maprnin  32748  nndiffz1  32794  ismnt  32957  mgcval  32961  omndmul2  33071  erler  33251  isorng  33308  opprnsg  33491  1arithidom  33544  1arithufdlem4  33554  smatrcl  33756  ordtconnlem1  33884  isrrext  33962  sigaex  34090  sigaval  34091  omssubaddlem  34280  omssubadd  34281  eulerpartleme  34344  eulerpartlemt0  34350  eulerpartlemr  34355  eulerpartlemn  34362  probun  34400  ballotlemelo  34468  ballotlem2  34469  ballotlemfc0  34473  ballotlemfcc  34474  reprdifc  34620  bnj248  34692  bnj250  34693  bnj268  34701  bnj312  34704  bnj945  34765  bnj110  34850  bnj849  34917  bnj882  34918  bnj893  34920  bnj916  34925  bnj983  34943  bnj1040  34964  bnj1175  34996  cusgredgex  35105  cusgr3cyclex  35120  erdszelem1  35175  iscvm  35243  elmpst  35520  mpstrcl  35525  dfso3  35699  xpab  35705  coepr  35732  dfdm5  35753  dfrn5  35754  elima4  35756  fv1stcnv  35757  fv2ndcnv  35758  brpprod  35866  dfon3  35873  elfix  35884  dffix2  35886  elfuns  35896  brimg  35918  brapply  35919  brsuccf  35922  funpartlem  35923  funpartfun  35924  brrestrict  35930  dfrecs2  35931  dfrdg4  35932  lineunray  36128  ellines  36133  rmoeqi  36168  reueqi  36170  itgeq12i  36187  finminlem  36300  fneval  36334  neibastop3  36344  eliminable-abelv  36851  bj-inrab  36909  bj-rest10  37070  bj-restpw  37074  bj-restuni  37079  bj-mpomptALT  37101  bj-imdirco  37172  icorempo  37333  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlpssretop  37346  pibt2  37399  wl-ifp-ncond2  37447  wl-df3-3mintru2  37468  wl-2mintru1  37472  rabiun  37579  iundif1  37580  lindsenlbs  37601  poimirlem4  37610  poimirlem25  37631  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnclem2  37658  itg2addnclem3  37659  itg2addnc  37660  ftc1anc  37687  isbnd2  37769  bndss  37772  heibor1lem  37795  heibor1  37796  isrngohom  37951  isidl  38000  sbccom2lem  38110  anan  38209  eqbrb  38213  eqelb  38215  br1cnvinxp  38237  eldmqsres  38268  idinxpssinxp2  38299  moantr  38345  inxpxrn  38376  dfcoss3  38395  cocossss  38417  ressn2  38423  br1cossinidres  38430  br1cossincnvepres  38431  br1cossxrnidres  38432  br1cossxrncnvepres  38433  refrelcoss2  38445  symrelcoss2  38447  cosscnvssid5  38459  br1cossxrncnvssrres  38489  dfrefrel3  38497  dfcnvrefrel3  38512  cosselcnvrefrels2  38519  cosselcnvrefrels3  38520  cosselcnvrefrels4  38521  cosselcnvrefrels5  38522  dfsymrel3  38531  refsymrel2  38548  refsymrel3  38549  elrefsymrels3  38551  dftrrel3  38559  dfeqvrel2  38571  dfeqvrel3  38572  redundpbi1  38612  refrelredund3  38618  eldmqs1cossres  38640  dffunALTV2  38669  dffunALTV3  38670  dffunALTV4  38671  dffunALTV5  38672  dfdisjALTV  38694  dfdisjALTV2  38695  dfdisjALTV3  38696  dfdisjALTV4  38697  eldisjs3  38705  eldisjs4  38706  disjsuc  38740  prtlem70  38838  prtlem100  38840  prter2  38862  lsateln0  38976  islshpat  38998  lcvnbtwn3  39009  islfl  39041  ishlat1  39333  ishlat2  39334  cvrat4  39425  islvol5  39561  psubspset  39726  snatpsubN  39732  dalawlem13  39865  psubclsetN  39918  isltrn2N  40102  cdlemftr3  40547  dibelval3  41129  dicval2  41161  dicopelval2  41163  dicelval2N  41164  dihglb2  41324  islpolN  41465  lcfls1c  41518  mapdvalc  41611  mapdval4N  41614  mapdordlem1a  41616  aks4d1p8  42068  fimgmcyc  42520  prjsperref  42592  prjspeclsp  42598  elmzpcl  42713  mzpindd  42733  fphpd  42803  pw2f1ocnv  43025  islmodfg  43057  islssfg2  43059  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  44405  opelopab4  44548  ax6e2nd  44555  en3lplem2VD  44841  ax6e2ndVD  44905  ax6e2ndALT  44927  iuneq1i  45024  ssrabf  45053  limcrecl  45584  dvnprodlem2  45902  fourierdlem103  46164  fourierdlem104  46165  4an21  47219  sprvalpwn0  47407  pairreueq  47434  dfvopnbgr2  47776  isubgredg  47789  xpsnopab  48000  sgrp2sgrp  48071  opeliun2xp  48177  mpomptx2  48179  lindslinindsimp1  48302  lindslinindsimp2  48308  itsclc0b  48621  mo0sn  48663  iscnrm3lem3  48731  isthincd2  48837  thinccic  48861  alsconv  49020  aacllem  49031