Theorem anbi1i 623

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi2ci  624  anbi12i  626  bianassc  639  anandi  672  pm5.53  999  dfifp4  1059  dfifp5  1060  3an4anass  1098  3ioran  1099  an6  1437  an3andi  1474  an33rean  1475  19.26-3an  1858  19.28v  1978  sb3an  2062  19.28  2197  eeeanv  2329  sbel2x  2458  eu6OLD  2621  eu6OLDOLD  2622  2eu4  2713  r19.26-3  3141  r19.41v  3310  r19.41  3311  rexcomOLD  3319  rexcomf  3321  3reeanv  3331  rabrab  3340  cbvreu  3403  ceqsex3v  3491  spc2ed  3546  rexab  3627  rexrab  3628  rmo4  3660  rmo3f  3664  reuind  3683  sbc3an  3772  rmo3  3806  rmo3OLD  3807  ssrab  3976  rexun  4093  elin3  4104  inass  4122  rexin  4142  dfun2  4162  indifdir  4186  difin2  4192  inrab2  4202  rabun2  4208  reuun2  4212  undif4  4336  rexdifpr  4509  rexsns  4520  rexdifsn  4640  2ralunsn  4738  iuncom4  4839  iindif1  4902  iunxiun  4924  disjxun  4966  zfrep4  5098  inuni  5144  reusv2lem4  5200  reusv2  5202  otth2  5274  copsexg  5280  copsex4g  5283  opelopabsbALT  5313  rabxp  5495  opeliunxp  5512  xpundir  5514  xpiundi  5515  xpiundir  5516  brinxp2  5522  copsex2gb  5572  dminss  5893  imainss  5894  difxp  5904  cnvresima  5969  coundi  5982  resco  5985  imaco  5986  rnco  5987  coiun  5991  coi1  5997  coass  6000  cnvpo  6020  xpco  6022  wfi  6063  dffun2  6242  fncnv  6304  imadif  6315  mptun  6369  dff1o2  6495  dff1o3  6496  brprcneu  6537  fvun2  6629  eqfnfv3  6676  respreima  6708  f1ompt  6745  f1ossf1o  6760  fsn  6767  fmptsng  6800  fmptsnd  6801  tpres  6837  abrexco  6875  imaiun  6876  f1mpt  6891  dff1o6  6904  oprabid  7054  dfoprab2  7078  oprab4  7103  mpomptx  7128  elpwpwel  7353  elxp4  7490  elxp5  7491  ffoss  7510  f11o  7511  opabex3d  7529  opabex3rd  7530  opabex3  7531  abexssex  7534  elxp7  7587  dfopab2  7613  dfoprab3s  7614  frxp  7680  xporderlem  7681  suppssov1  7720  suppssfv  7724  brtpos2  7756  tpostpos  7770  tposmpo  7787  wfrfun  7824  dfrecs3  7868  oarec  8045  oeeu  8086  mapsncnv  8313  dfixp  8319  domen  8377  xpsnen  8455  xpcomco  8461  xpassen  8465  sbthlem9  8489  frfi  8616  marypha2lem2  8753  epfrs  9026  tcsni  9038  cp  9173  dfac5lem1  9402  dfac5lem2  9403  dfac5lem5  9406  kmlem3  9431  dfackm  9445  cfval2  9535  cflim3  9537  cfss  9540  cfslb  9541  zfcndrep  9889  eltsk2g  10026  ltexpi  10177  recmulnq  10239  ltexprlem4  10314  addsrpr  10350  mulsrpr  10351  addcnsr  10410  mulcnsr  10411  ltresr  10415  axrrecex  10438  elnnz  11845  elnn0z  11848  fnn0ind  11935  rexuz2  12152  rexrp  12264  elixx3g  12605  elfz2  12753  elfzuzb  12756  fznn  12829  elfz2nn0  12852  fznn0  12853  4fvwrd4  12881  preduz  12883  elfzo2  12895  fzind2  13009  hashgt23el  13637  hashf1lem1  13665  hashf1lem2  13666  fz1isolem  13671  s4f1o  14120  wwlktovfo  14160  fsum2dlem  14962  modfsummod  14986  sinltx  15379  divalglem10  15590  divalgb  15592  coprmproddvdslem  15839  isprm2  15859  infpn2  16082  prdsle  16568  prdsless  16569  prdsleval  16583  imasleval  16647  xpscf  16671  dfiso2  16875  oppcsect  16881  elhoma  17125  ispos2  17391  lubeldm  17424  glbeldm  17437  tosso  17479  ismhm  17780  issubm  17790  submacs  17808  issubg  18037  issubg3  18055  gaorb  18182  pmtrrn2  18323  efgcpbllema  18611  efgcpbllemb  18612  frgpuplem  18629  subgdmdprd  18877  dprd2d2  18887  dfrhm2  19163  drngprop  19207  drngid2  19212  opprdrng  19220  issubrg  19229  isabv  19284  islss  19400  islbs  19542  lsmspsn  19550  isassa  19781  aspval2  19819  ltbval  19943  opsrle  19947  opsrtoslem1  19955  isobs  20550  islinds  20639  fvmptnn04if  21145  ntreq0  21373  restntr  21478  cnnei  21578  hausnei2  21649  cmpcov2  21686  cmpsub  21696  uncmp  21699  cmpfi  21704  llyi  21770  dissnlocfin  21825  iskgen3  21845  1stckgenlem  21849  ptpjpre1  21867  txcnpi  21904  txtube  21936  hausdiag  21941  txlm  21944  txkgen  21948  cfinfil  22189  csdfil  22190  supfil  22191  fin1aufil  22228  elflim2  22260  hauspwpwf1  22283  txflf  22302  isfcls  22305  alexsubALTlem3  22345  alexsubALT  22347  cnextcn  22363  istmd  22370  istgp  22373  tgphaus  22412  qustgplem  22416  istrg  22459  istdrg  22461  istlm  22480  blres  22728  isms2  22747  metrest  22821  metuel2  22862  restmetu  22867  isngp  22892  isnlm  22971  elii1  23226  isclmp  23388  iscvsp  23419  isncvsngp  23440  iscph  23461  cfilucfil3  23610  isbn  23628  limcrcl  24159  ig1pval3  24455  plydivex  24573  ellogdm  24907  cubic  25112  dmarea  25221  vmasum  25478  lgsquadlem1  25642  lgsquadlem2  25643  istrkg3ld  25933  legov  26057  ltgov  26069  colinearalg  26383  axeuclid  26436  axcontlem2  26438  axcontlem5  26441  nbgrel  26809  nbupgrres  26833  nbusgredgeu0  26837  nb3grprlem2  26850  nb3grpr2  26852  nb3gr2nb  26853  cplgr3v  26904  finsumvtxdg2ssteplem3  27016  wlkonprop  27126  upgrtrls  27169  upgristrl  27170  wksonproplem  27172  usgr2pth0  27232  wwlksnext  27357  wwlksnextsurj  27364  wwlksnfi  27370  wwlksnfiOLD  27371  wspthsnwspthsnon  27381  wpthswwlks2on  27426  rusgrnumwwlkl1  27433  erclwwlkref  27484  isclwwlknx  27500  clwwlknwwlksn  27502  erclwwlknref  27534  clwlknf1oclwwlkn  27549  clwwlknonel  27560  clwwlknon1  27562  clwwlknon2x  27568  clwwlkvbij  27578  iseupthf1o  27667  2pthfrgrrn  27749  fusgr2wsp2nb  27801  numclwwlk1lem2f1  27824  numclwwlkovh  27840  numclwlk2lem2f1o  27846  frgrregord013  27862  avril1  27929  islno  28217  h2hlm  28444  hcau  28648  hhsssh2  28734  dfch2  28871  elcnop  29321  ellnop  29322  elhmop  29337  elcnfn  29346  ellnfn  29347  dmadjss  29351  adjeu  29353  adjval  29354  hhcno  29368  hhcnf  29369  eleigvec  29421  isst  29677  ishst  29678  cvnbtwn3  29752  cvnbtwn4  29753  chirredi  29858  sumdmdii  29879  or3di  29912  rexunirn  29944  rmoun  29946  dmrab  29948  difrab2  29949  iunin1f  29995  disjunsn  30030  opeldifid  30035  ofpreima  30096  mpomptxf  30111  1stpreima  30126  2ndpreima  30127  f1od2  30141  resf1o  30150  maprnin  30151  nndiffz1  30193  omndmul2  30369  isorng  30522  smatrcl  30672  ordtconnlem1  30780  isrrext  30854  sigaex  30982  sigaval  30983  omssubaddlem  31170  omssubadd  31171  eulerpartleme  31234  eulerpartlemt0  31240  eulerpartlemr  31245  eulerpartlemn  31252  probun  31290  ballotlemelo  31358  ballotlem2  31359  ballotlemfc0  31363  ballotlemfcc  31364  reprdifc  31511  bnj248  31583  bnj250  31584  bnj268  31592  bnj312  31595  bnj945  31658  bnj110  31742  bnj849  31809  bnj882  31810  bnj893  31812  bnj916  31817  bnj983  31835  bnj1040  31854  bnj1175  31886  cusgredgex  31978  cusgr3cyclex  31993  erdszelem1  32048  iscvm  32116  elmpst  32393  mpstrcl  32398  dfso3  32560  coepr  32598  dfpo2  32601  dfdm5  32626  dfrn5  32627  elima4  32629  fv1stcnv  32630  fv2ndcnv  32631  frpoind  32691  frind  32696  soseq  32707  elno3  32773  slenlt  32842  madeval2  32901  brpprod  32957  dfon3  32964  elfix  32975  dffix2  32977  elfuns  32987  brimg  33009  brapply  33010  brsuccf  33013  funpartlem  33014  funpartfun  33015  brrestrict  33021  dfrecs2  33022  dfrdg4  33023  lineunray  33219  ellines  33224  finminlem  33277  fneval  33311  neibastop3  33321  bj-inrab  33822  bj-rest10  33999  bj-restpw  34003  bj-restuni  34008  bj-mpomptALT  34030  bj-elid3  34050  icorempo  34184  isbasisrelowllem1  34188  isbasisrelowllem2  34189  relowlpssretop  34197  pibt2  34250  rabiun  34417  iundif1  34418  lindsenlbs  34439  poimirlem4  34448  poimirlem25  34469  poimirlem26  34470  poimirlem29  34473  poimirlem30  34474  ismblfin  34485  ovoliunnfl  34486  voliunnfl  34488  volsupnfl  34489  itg2addnclem2  34496  itg2addnclem3  34497  itg2addnc  34498  ftc1anc  34527  isbnd2  34614  bndss  34617  heibor1lem  34640  heibor1  34641  isrngohom  34796  isidl  34845  sbccom2lem  34955  anan  35052  eqelb  35055  eldmqsres  35096  idinxpssinxp2  35128  moantr  35169  inxpxrn  35195  dfcoss3  35214  cocossss  35233  br1cossinidres  35241  br1cossincnvepres  35242  br1cossxrnidres  35243  br1cossxrncnvepres  35244  refrelcoss2  35256  symrelcoss2  35258  cosscnvssid5  35270  br1cossxrncnvssrres  35300  dfrefrel3  35308  dfcnvrefrel3  35321  cosselcnvrefrels2  35326  cosselcnvrefrels3  35327  cosselcnvrefrels4  35328  cosselcnvrefrels5  35329  dfsymrel3  35338  refsymrel2  35355  refsymrel3  35356  elrefsymrels3  35358  dftrrel3  35366  dfeqvrel2  35377  dfeqvrel3  35378  redundpbi1  35418  refrelredund3  35424  eldmqs1cossres  35445  dffunALTV2  35473  dffunALTV3  35474  dffunALTV4  35475  dffunALTV5  35476  dfdisjALTV  35498  dfdisjALTV2  35499  dfdisjALTV3  35500  dfdisjALTV4  35501  eldisjs3  35509  eldisjs4  35510  prtlem70  35545  prtlem100  35547  prter2  35569  lsateln0  35683  islshpat  35705  lcvnbtwn3  35716  islfl  35748  ishlat1  36040  ishlat2  36041  cvrat4  36131  islvol5  36267  psubspset  36432  snatpsubN  36438  dalawlem13  36571  psubclsetN  36624  isltrn2N  36808  cdlemftr3  37253  dibelval3  37835  dicval2  37867  dicopelval2  37869  dicelval2N  37870  dihglb2  38030  islpolN  38171  lcfls1c  38224  mapdvalc  38317  mapdval4N  38320  mapdordlem1a  38322  prjsperref  38774  prjspeclsp  38780  elmzpcl  38829  mzpindd  38849  fphpd  38919  pw2f1ocnv  39140  islmodfg  39175  islssfg2  39177  isdomn3  39310  rp-isfinite6  39390  elmapintrab  39442  elinintrab  39443  relintab  39449  dfrtrcl5  39495  fsovrfovd  39861  ntrk1k3eqk13  39906  gneispace3  39989  k0004lem1  40003  pm13.192  40301  opelopab4  40445  ax6e2nd  40452  en3lplem2VD  40738  ax6e2ndVD  40802  ax6e2ndALT  40824  ssrabf  40942  limcrecl  41473  dvnprodlem2  41795  fourierdlem103  42058  fourierdlem104  42059  4an21  43007  sprvalpwn0  43149  pairreueq  43176  xpsnopab  43536  ismgmhm  43554  issubmgm  43560  submgmacs  43575  sgrp2sgrp  43635  opeliun2xp  43881  mpomptx2  43883  lindslinindsimp1  44014  lindslinindsimp2  44020  itsclc0b  44262  alsconv  44393  aacllem  44404