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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anbi2ci  626  anbi12i  628  bianassc  641  anandi  674  pm5.53  1003  dfifp4  1065  dfifp5  1066  3an4anass  1105  3ioran  1106  an6  1445  an3andi  1482  an33rean  1483  an33reanOLD  1484  19.26-3an  1873  19.28v  1992  sb3an  2082  19.28  2219  eeeanv  2346  sbel2x  2472  2eu4  2654  r19.26-3  3112  r19.41v  3182  3reeanv  3215  r19.41  3243  rexcomf  3307  rabrab  3323  cbvreuwOLD  3389  cbvreu  3393  rabeqi  3423  rabrabi  3434  ceqsex3v  3489  spc2ed  3545  rexabOLD  3637  rexrab  3638  rmo4  3670  rmo3f  3674  reuind  3693  sbc3an  3791  rmo3  3827  ssrab  4012  rexun  4130  elin3  4140  inass  4159  rexin  4179  dfun2  4199  indifdirOLD  4225  difin2  4231  inrab2  4247  rabun2  4253  reuun2  4254  undif4  4406  rexdifpr  4598  rexsns  4609  rexdifsn  4733  2ralunsn  4831  iuncom4  4939  iindif1  5011  iunxiun  5033  disjxun  5079  zfrep4  5229  inuni  5276  reusv2lem4  5333  reusv2  5335  otth2  5411  copsexgw  5417  copsexg  5418  copsex2g  5420  copsex4g  5422  vopelopabsb  5455  rabxp  5646  opeliunxp  5665  xpundir  5667  xpiundi  5668  xpiundir  5669  brinxp2  5675  copsex2gb  5728  dminss  6071  imainss  6072  difxp  6082  cnvresima  6148  coundi  6165  resco  6168  imaco  6169  rnco  6170  coiun  6174  coi1  6180  coass  6183  cnvpo  6205  xpco  6207  dfpo2  6214  frpoind  6260  wfiOLD  6269  dffun2  6468  dffun2OLD  6469  dffun2OLDOLD  6470  fncnv  6536  imadif  6547  mptun  6609  ffrnb  6645  dff1o2  6751  dff1o3  6752  brprcneu  6794  brprcneuALT  6795  fvun2  6892  eqfnfv3  6943  respreima  6975  f1ompt  7017  f1ossf1o  7032  fsn  7039  fmptsng  7072  fmptsnd  7073  tpres  7108  abrexco  7149  imaiun  7150  f1mpt  7166  dff1o6  7179  oprabidw  7338  oprabid  7339  dfoprab2  7365  oprab4  7393  mpomptx  7419  elpwpwel  7649  elxp4  7801  elxp5  7802  ffoss  7820  f11o  7821  opabex3d  7840  opabex3rd  7841  opabex3  7842  abexssex  7845  elxp7  7898  dfopab2  7924  dfoprab3s  7925  fsplit  7989  frxp  7998  xporderlem  7999  suppssov1  8045  suppssfv  8049  brtpos2  8079  tpostpos  8093  tposmpo  8110  wfrfunOLD  8181  dfrecs3  8234  dfrecs3OLD  8235  oarec  8424  oeeu  8465  eldifsucnn  8525  mapsncnv  8712  dfixp  8718  domen  8782  xpsnen  8880  xpcomco  8887  xpassen  8891  sbthlem9  8916  frfi  9103  marypha2lem2  9239  brttrcl2  9516  epfrs  9533  tcsni  9545  frind  9552  cp  9693  dfac5lem1  9925  dfac5lem2  9926  dfac5lem5  9929  kmlem3  9954  dfackm  9968  cfval2  10062  cflim3  10064  cfss  10067  cfslb  10068  zfcndrep  10416  eltsk2g  10553  ltexpi  10704  recmulnq  10766  ltexprlem4  10841  addsrpr  10877  mulsrpr  10878  addcnsr  10937  mulcnsr  10938  ltresr  10942  axrrecex  10965  elnnz  12375  elnn0z  12378  fnn0ind  12465  rexuz2  12685  rexrp  12797  elixx3g  13138  elfz2  13292  elfzuzb  13296  fznn  13370  elfz2nn0  13393  fznn0  13394  4fvwrd4  13422  preduz  13424  elfzo2  13436  fzind2  13551  hashgt23el  14184  hashf1lem1  14213  hashf1lem1OLD  14214  hashf1lem2  14215  fz1isolem  14220  s4f1o  14676  wwlktovfo  14718  fsum2dlem  15527  modfsummod  15551  sinltx  15943  divalglem10  16156  divalgb  16158  coprmproddvdslem  16412  isprm2  16432  infpn2  16659  prdsle  17218  prdsless  17219  prdsleval  17233  imasleval  17297  xpscf  17321  dfiso2  17529  oppcsect  17535  elhoma  17792  ispos2  18078  lubeldm  18116  glbeldm  18129  tosso  18182  ismhm  18477  issubm  18487  submacs  18510  issubg  18800  issubg3  18818  gaorb  18958  pmtrrn2  19113  efgcpbllema  19405  efgcpbllemb  19406  frgpuplem  19423  subgdmdprd  19682  dprd2d2  19692  dfrhm2  20006  drngprop  20047  drngid2  20052  opprdrng  20060  issubrg  20069  isabv  20124  islss  20241  islbs  20383  lsmspsn  20391  isobs  20972  islinds  21061  isassa  21108  aspval2  21147  ltbval  21289  opsrle  21293  opsrtoslem1  21307  fvmptnn04if  22043  ntreq0  22273  restntr  22378  cnnei  22478  hausnei2  22549  cmpcov2  22586  cmpsub  22596  uncmp  22599  cmpfi  22604  llyi  22670  dissnlocfin  22725  iskgen3  22745  1stckgenlem  22749  ptpjpre1  22767  txcnpi  22804  txtube  22836  hausdiag  22841  txlm  22844  txkgen  22848  cfinfil  23089  csdfil  23090  supfil  23091  fin1aufil  23128  elflim2  23160  hauspwpwf1  23183  txflf  23202  isfcls  23205  alexsubALTlem3  23245  alexsubALT  23247  cnextcn  23263  istmd  23270  istgp  23273  tgphaus  23313  qustgplem  23317  istrg  23360  istdrg  23362  istlm  23381  blres  23629  isms2  23648  metrest  23725  metuel2  23766  restmetu  23771  isngp  23797  isnlm  23884  elii1  24143  isclmp  24305  iscvsp  24336  isncvsngp  24358  iscph  24379  cfilucfil3  24529  isbn  24547  limcrcl  25083  ig1pval3  25384  plydivex  25502  ellogdm  25839  cubic  26044  dmarea  26152  vmasum  26409  lgsquadlem1  26573  lgsquadlem2  26574  istrkg3ld  26867  legov  26991  ltgov  27003  colinearalg  27323  axeuclid  27376  axcontlem2  27378  axcontlem5  27381  nbgrel  27752  nbupgrres  27776  nbusgredgeu0  27780  nb3grprlem2  27793  nb3grpr2  27795  nb3gr2nb  27796  cplgr3v  27847  finsumvtxdg2ssteplem3  27959  wlkonprop  28071  upgrtrls  28114  upgristrl  28115  wksonproplem  28117  wksonproplemOLD  28118  usgr2pth0  28178  wwlksnext  28303  wwlksnextsurj  28310  wwlksnfi  28316  wspthsnwspthsnon  28326  wpthswwlks2on  28371  rusgrnumwwlkl1  28378  erclwwlkref  28429  isclwwlknx  28445  clwwlknwwlksn  28447  clwwlkel  28455  erclwwlknref  28478  clwlknf1oclwwlkn  28493  clwwlknonel  28504  clwwlknon1  28506  clwwlknon2x  28512  clwwlkvbij  28522  iseupthf1o  28611  2pthfrgrrn  28691  fusgr2wsp2nb  28743  numclwwlk1lem2f1  28766  numclwwlkovh  28782  numclwlk2lem2f1o  28788  frgrregord013  28804  avril1  28872  islno  29160  h2hlm  29387  hcau  29591  hhsssh2  29677  dfch2  29814  elcnop  30264  ellnop  30265  elhmop  30280  elcnfn  30289  ellnfn  30290  dmadjss  30294  adjeu  30296  adjval  30297  hhcno  30311  hhcnf  30312  eleigvec  30364  isst  30620  ishst  30621  cvnbtwn3  30695  cvnbtwn4  30696  chirredi  30801  sumdmdii  30822  or3di  30855  rexunirn  30885  rmoun  30887  dmrab  30889  difrab2  30890  iunin1f  30942  disjunsn  30978  opeldifid  30983  ofpreima  31047  mpomptxf  31061  1stpreima  31084  2ndpreima  31085  f1od2  31101  resf1o  31110  maprnin  31111  nndiffz1  31152  ismnt  31306  mgcval  31310  omndmul2  31383  isorng  31543  smatrcl  31791  ordtconnlem1  31919  isrrext  31995  sigaex  32123  sigaval  32124  omssubaddlem  32311  omssubadd  32312  eulerpartleme  32375  eulerpartlemt0  32381  eulerpartlemr  32386  eulerpartlemn  32393  probun  32431  ballotlemelo  32499  ballotlem2  32500  ballotlemfc0  32504  ballotlemfcc  32505  reprdifc  32652  bnj248  32724  bnj250  32725  bnj268  32733  bnj312  32736  bnj945  32798  bnj110  32883  bnj849  32950  bnj882  32951  bnj893  32953  bnj916  32958  bnj983  32976  bnj1040  32997  bnj1175  33029  cusgredgex  33128  cusgr3cyclex  33143  erdszelem1  33198  iscvm  33266  elmpst  33543  mpstrcl  33548  dfso3  33709  riotarab  33718  reurab  33719  xpab  33722  ot2elxp  33724  imaeqsexv  33735  coepr  33765  dfdm5  33792  dfrn5  33793  elima4  33795  fv1stcnv  33796  fv2ndcnv  33797  soseq  33848  elno3  33903  slenlt  34000  madeval2  34082  brpprod  34232  dfon3  34239  elfix  34250  dffix2  34252  elfuns  34262  brimg  34284  brapply  34285  brsuccf  34288  funpartlem  34289  funpartfun  34290  brrestrict  34296  dfrecs2  34297  dfrdg4  34298  lineunray  34494  ellines  34499  finminlem  34552  fneval  34586  neibastop3  34596  eliminable-abelv  35097  bj-inrab  35159  bj-rest10  35303  bj-restpw  35307  bj-restuni  35312  bj-mpomptALT  35334  bj-imdirco  35405  icorempo  35566  isbasisrelowllem1  35570  isbasisrelowllem2  35571  relowlpssretop  35579  pibt2  35632  wl-ifp-ncond2  35680  wl-df3-3mintru2  35701  wl-2mintru1  35705  rabiun  35794  iundif1  35795  lindsenlbs  35816  poimirlem4  35825  poimirlem25  35846  poimirlem26  35847  poimirlem29  35850  poimirlem30  35851  ismblfin  35862  ovoliunnfl  35863  voliunnfl  35865  volsupnfl  35866  itg2addnclem2  35873  itg2addnclem3  35874  itg2addnc  35875  ftc1anc  35902  isbnd2  35985  bndss  35988  heibor1lem  36011  heibor1  36012  isrngohom  36167  isidl  36216  sbccom2lem  36326  anan  36423  eqelb  36426  eldmqsres  36464  idinxpssinxp2  36495  moantr  36536  inxpxrn  36563  dfcoss3  36582  cocossss  36601  br1cossinidres  36609  br1cossincnvepres  36610  br1cossxrnidres  36611  br1cossxrncnvepres  36612  refrelcoss2  36624  symrelcoss2  36626  cosscnvssid5  36638  br1cossxrncnvssrres  36668  dfrefrel3  36676  dfcnvrefrel3  36689  cosselcnvrefrels2  36694  cosselcnvrefrels3  36695  cosselcnvrefrels4  36696  cosselcnvrefrels5  36697  dfsymrel3  36706  refsymrel2  36723  refsymrel3  36724  elrefsymrels3  36726  dftrrel3  36734  dfeqvrel2  36745  dfeqvrel3  36746  redundpbi1  36786  refrelredund3  36792  eldmqs1cossres  36813  dffunALTV2  36841  dffunALTV3  36842  dffunALTV4  36843  dffunALTV5  36844  dfdisjALTV  36866  dfdisjALTV2  36867  dfdisjALTV3  36868  dfdisjALTV4  36869  eldisjs3  36877  eldisjs4  36878  prtlem70  36913  prtlem100  36915  prter2  36937  lsateln0  37051  islshpat  37073  lcvnbtwn3  37084  islfl  37116  ishlat1  37408  ishlat2  37409  cvrat4  37499  islvol5  37635  psubspset  37800  snatpsubN  37806  dalawlem13  37939  psubclsetN  37992  isltrn2N  38176  cdlemftr3  38621  dibelval3  39203  dicval2  39235  dicopelval2  39237  dicelval2N  39238  dihglb2  39398  islpolN  39539  lcfls1c  39592  mapdvalc  39685  mapdval4N  39688  mapdordlem1a  39690  aks4d1p8  40137  prjsperref  40482  prjspeclsp  40488  elmzpcl  40585  mzpindd  40605  fphpd  40675  pw2f1ocnv  40897  islmodfg  40932  islssfg2  40934  isdomn3  41067  rp-isfinite6  41163  minregex  41179  elmapintrab  41222  elinintrab  41223  relintab  41229  dfrtrcl5  41275  fsovrfovd  41655  ntrk1k3eqk13  41698  gneispace3  41781  k0004lem1  41795  pm13.192  42066  opelopab4  42209  ax6e2nd  42216  en3lplem2VD  42502  ax6e2ndVD  42566  ax6e2ndALT  42588  ssrabf  42702  limcrecl  43219  dvnprodlem2  43537  fourierdlem103  43799  fourierdlem104  43800  4an21  44820  sprvalpwn0  44993  pairreueq  45020  xpsnopab  45377  ismgmhm  45395  issubmgm  45401  submgmacs  45416  sgrp2sgrp  45480  opeliun2xp  45726  mpomptx2  45728  lindslinindsimp1  45856  lindslinindsimp2  45862  itsclc0b  46176  mo0sn  46219  iscnrm3lem3  46287  isthincd2  46377  thinccic  46400  alsconv  46552  aacllem  46563