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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi2ci  624  anbi12i  626  bianassc  639  anandi  672  pm5.53  1001  dfifp4  1063  dfifp5  1064  3an4anass  1103  3ioran  1104  an6  1443  an3andi  1480  an33rean  1481  an33reanOLD  1482  19.26-3an  1878  19.28v  1997  sb3an  2087  19.28  2224  eeeanv  2351  sbel2x  2475  2eu4  2657  r19.26-3  3098  r19.41v  3275  r19.41  3276  rexcomf  3285  3reeanv  3295  rabrab  3309  cbvreuw  3373  cbvreu  3378  rabeqi  3414  rabrabi  3425  ceqsex3v  3482  spc2ed  3538  rexabOLD  3633  rexrab  3634  rmo4  3668  rmo3f  3672  reuind  3691  sbc3an  3790  rmo3  3826  ssrab  4010  rexun  4128  elin3  4138  inass  4158  rexin  4178  dfun2  4198  indifdirOLD  4224  difin2  4230  inrab2  4246  rabun2  4252  reuun2  4253  undif4  4405  rexdifpr  4599  rexsns  4610  rexdifsn  4732  2ralunsn  4831  iuncom4  4937  iindif1  5008  iunxiun  5030  disjxun  5076  zfrep4  5223  inuni  5270  reusv2lem4  5327  reusv2  5329  otth2  5400  copsexgw  5406  copsexg  5407  copsex2g  5409  copsex4g  5411  vopelopabsb  5443  rabxp  5634  opeliunxp  5653  xpundir  5655  xpiundi  5656  xpiundir  5657  brinxp2  5663  copsex2gb  5713  dminss  6053  imainss  6054  difxp  6064  cnvresima  6130  coundi  6148  resco  6151  imaco  6152  rnco  6153  coiun  6157  coi1  6163  coass  6166  cnvpo  6187  xpco  6189  dfpo2  6196  frpoind  6242  wfiOLD  6251  dffun2  6440  fncnv  6503  imadif  6514  mptun  6575  ffrnb  6611  dff1o2  6717  dff1o3  6718  brprcneu  6759  fvprc  6760  fvun2  6854  eqfnfv3  6905  respreima  6937  f1ompt  6979  f1ossf1o  6994  fsn  7001  fmptsng  7034  fmptsnd  7035  tpres  7070  abrexco  7111  imaiun  7112  f1mpt  7128  dff1o6  7141  oprabidw  7299  oprabid  7300  dfoprab2  7324  oprab4  7352  mpomptx  7378  elpwpwel  7608  elxp4  7756  elxp5  7757  ffoss  7775  f11o  7776  opabex3d  7794  opabex3rd  7795  opabex3  7796  abexssex  7799  elxp7  7852  dfopab2  7878  dfoprab3s  7879  fsplit  7941  frxp  7951  xporderlem  7952  suppssov1  7998  suppssfv  8002  brtpos2  8032  tpostpos  8046  tposmpo  8063  wfrfunOLD  8134  dfrecs3  8187  dfrecs3OLD  8188  oarec  8369  oeeu  8410  eldifsucnn  8468  mapsncnv  8655  dfixp  8661  domen  8722  xpsnen  8812  xpcomco  8818  xpassen  8822  sbthlem9  8847  frfi  9020  marypha2lem2  9156  brttrcl2  9433  epfrs  9472  tcsni  9484  frind  9492  cp  9633  dfac5lem1  9863  dfac5lem2  9864  dfac5lem5  9867  kmlem3  9892  dfackm  9906  cfval2  10000  cflim3  10002  cfss  10005  cfslb  10006  zfcndrep  10354  eltsk2g  10491  ltexpi  10642  recmulnq  10704  ltexprlem4  10779  addsrpr  10815  mulsrpr  10816  addcnsr  10875  mulcnsr  10876  ltresr  10880  axrrecex  10903  elnnz  12312  elnn0z  12315  fnn0ind  12402  rexuz2  12621  rexrp  12733  elixx3g  13074  elfz2  13228  elfzuzb  13232  fznn  13306  elfz2nn0  13329  fznn0  13330  4fvwrd4  13358  preduz  13360  elfzo2  13372  fzind2  13486  hashgt23el  14120  hashf1lem1  14149  hashf1lem1OLD  14150  hashf1lem2  14151  fz1isolem  14156  s4f1o  14612  wwlktovfo  14654  fsum2dlem  15463  modfsummod  15487  sinltx  15879  divalglem10  16092  divalgb  16094  coprmproddvdslem  16348  isprm2  16368  infpn2  16595  prdsle  17154  prdsless  17155  prdsleval  17169  imasleval  17233  xpscf  17257  dfiso2  17465  oppcsect  17471  elhoma  17728  ispos2  18014  lubeldm  18052  glbeldm  18065  tosso  18118  ismhm  18413  issubm  18423  submacs  18446  issubg  18736  issubg3  18754  gaorb  18894  pmtrrn2  19049  efgcpbllema  19341  efgcpbllemb  19342  frgpuplem  19359  subgdmdprd  19618  dprd2d2  19628  dfrhm2  19942  drngprop  19983  drngid2  19988  opprdrng  19996  issubrg  20005  isabv  20060  islss  20177  islbs  20319  lsmspsn  20327  isobs  20908  islinds  20997  isassa  21044  aspval2  21083  ltbval  21225  opsrle  21229  opsrtoslem1  21243  fvmptnn04if  21979  ntreq0  22209  restntr  22314  cnnei  22414  hausnei2  22485  cmpcov2  22522  cmpsub  22532  uncmp  22535  cmpfi  22540  llyi  22606  dissnlocfin  22661  iskgen3  22681  1stckgenlem  22685  ptpjpre1  22703  txcnpi  22740  txtube  22772  hausdiag  22777  txlm  22780  txkgen  22784  cfinfil  23025  csdfil  23026  supfil  23027  fin1aufil  23064  elflim2  23096  hauspwpwf1  23119  txflf  23138  isfcls  23141  alexsubALTlem3  23181  alexsubALT  23183  cnextcn  23199  istmd  23206  istgp  23209  tgphaus  23249  qustgplem  23253  istrg  23296  istdrg  23298  istlm  23317  blres  23565  isms2  23584  metrest  23661  metuel2  23702  restmetu  23707  isngp  23733  isnlm  23820  elii1  24079  isclmp  24241  iscvsp  24272  isncvsngp  24294  iscph  24315  cfilucfil3  24465  isbn  24483  limcrcl  25019  ig1pval3  25320  plydivex  25438  ellogdm  25775  cubic  25980  dmarea  26088  vmasum  26345  lgsquadlem1  26509  lgsquadlem2  26510  istrkg3ld  26803  legov  26927  ltgov  26939  colinearalg  27259  axeuclid  27312  axcontlem2  27314  axcontlem5  27317  nbgrel  27688  nbupgrres  27712  nbusgredgeu0  27716  nb3grprlem2  27729  nb3grpr2  27731  nb3gr2nb  27732  cplgr3v  27783  finsumvtxdg2ssteplem3  27895  wlkonprop  28006  upgrtrls  28049  upgristrl  28050  wksonproplem  28052  usgr2pth0  28112  wwlksnext  28237  wwlksnextsurj  28244  wwlksnfi  28250  wspthsnwspthsnon  28260  wpthswwlks2on  28305  rusgrnumwwlkl1  28312  erclwwlkref  28363  isclwwlknx  28379  clwwlknwwlksn  28381  clwwlkel  28389  erclwwlknref  28412  clwlknf1oclwwlkn  28427  clwwlknonel  28438  clwwlknon1  28440  clwwlknon2x  28446  clwwlkvbij  28456  iseupthf1o  28545  2pthfrgrrn  28625  fusgr2wsp2nb  28677  numclwwlk1lem2f1  28700  numclwwlkovh  28716  numclwlk2lem2f1o  28722  frgrregord013  28738  avril1  28806  islno  29094  h2hlm  29321  hcau  29525  hhsssh2  29611  dfch2  29748  elcnop  30198  ellnop  30199  elhmop  30214  elcnfn  30223  ellnfn  30224  dmadjss  30228  adjeu  30230  adjval  30231  hhcno  30245  hhcnf  30246  eleigvec  30298  isst  30554  ishst  30555  cvnbtwn3  30629  cvnbtwn4  30630  chirredi  30735  sumdmdii  30756  or3di  30789  rexunirn  30819  rmoun  30821  dmrab  30823  difrab2  30824  iunin1f  30876  disjunsn  30912  opeldifid  30917  ofpreima  30981  mpomptxf  30995  1stpreima  31018  2ndpreima  31019  f1od2  31035  resf1o  31044  maprnin  31045  nndiffz1  31086  ismnt  31240  mgcval  31244  omndmul2  31317  isorng  31477  smatrcl  31725  ordtconnlem1  31853  isrrext  31929  sigaex  32057  sigaval  32058  omssubaddlem  32245  omssubadd  32246  eulerpartleme  32309  eulerpartlemt0  32315  eulerpartlemr  32320  eulerpartlemn  32327  probun  32365  ballotlemelo  32433  ballotlem2  32434  ballotlemfc0  32438  ballotlemfcc  32439  reprdifc  32586  bnj248  32658  bnj250  32659  bnj268  32667  bnj312  32670  bnj945  32732  bnj110  32817  bnj849  32884  bnj882  32885  bnj893  32887  bnj916  32892  bnj983  32910  bnj1040  32931  bnj1175  32963  cusgredgex  33062  cusgr3cyclex  33077  erdszelem1  33132  iscvm  33200  elmpst  33477  mpstrcl  33482  dfso3  33643  riotarab  33652  reurab  33653  xpab  33656  ot2elxp  33658  imaeqsexv  33669  coepr  33699  dfdm5  33726  dfrn5  33727  elima4  33729  fv1stcnv  33730  fv2ndcnv  33731  soseq  33782  elno3  33837  slenlt  33934  madeval2  34016  brpprod  34166  dfon3  34173  elfix  34184  dffix2  34186  elfuns  34196  brimg  34218  brapply  34219  brsuccf  34222  funpartlem  34223  funpartfun  34224  brrestrict  34230  dfrecs2  34231  dfrdg4  34232  lineunray  34428  ellines  34433  finminlem  34486  fneval  34520  neibastop3  34530  eliminable-abelv  35032  bj-inrab  35094  bj-rest10  35238  bj-restpw  35242  bj-restuni  35247  bj-mpomptALT  35269  bj-imdirco  35340  icorempo  35501  isbasisrelowllem1  35505  isbasisrelowllem2  35506  relowlpssretop  35514  pibt2  35567  wl-ifp-ncond2  35615  wl-df3-3mintru2  35636  wl-2mintru1  35640  rabiun  35729  iundif1  35730  lindsenlbs  35751  poimirlem4  35760  poimirlem25  35781  poimirlem26  35782  poimirlem29  35785  poimirlem30  35786  ismblfin  35797  ovoliunnfl  35798  voliunnfl  35800  volsupnfl  35801  itg2addnclem2  35808  itg2addnclem3  35809  itg2addnc  35810  ftc1anc  35837  isbnd2  35920  bndss  35923  heibor1lem  35946  heibor1  35947  isrngohom  36102  isidl  36151  sbccom2lem  36261  anan  36358  eqelb  36361  eldmqsres  36400  idinxpssinxp2  36432  moantr  36473  inxpxrn  36500  dfcoss3  36519  cocossss  36538  br1cossinidres  36546  br1cossincnvepres  36547  br1cossxrnidres  36548  br1cossxrncnvepres  36549  refrelcoss2  36561  symrelcoss2  36563  cosscnvssid5  36575  br1cossxrncnvssrres  36605  dfrefrel3  36613  dfcnvrefrel3  36626  cosselcnvrefrels2  36631  cosselcnvrefrels3  36632  cosselcnvrefrels4  36633  cosselcnvrefrels5  36634  dfsymrel3  36643  refsymrel2  36660  refsymrel3  36661  elrefsymrels3  36663  dftrrel3  36671  dfeqvrel2  36682  dfeqvrel3  36683  redundpbi1  36723  refrelredund3  36729  eldmqs1cossres  36750  dffunALTV2  36778  dffunALTV3  36779  dffunALTV4  36780  dffunALTV5  36781  dfdisjALTV  36803  dfdisjALTV2  36804  dfdisjALTV3  36805  dfdisjALTV4  36806  eldisjs3  36814  eldisjs4  36815  prtlem70  36850  prtlem100  36852  prter2  36874  lsateln0  36988  islshpat  37010  lcvnbtwn3  37021  islfl  37053  ishlat1  37345  ishlat2  37346  cvrat4  37436  islvol5  37572  psubspset  37737  snatpsubN  37743  dalawlem13  37876  psubclsetN  37929  isltrn2N  38113  cdlemftr3  38558  dibelval3  39140  dicval2  39172  dicopelval2  39174  dicelval2N  39175  dihglb2  39335  islpolN  39476  lcfls1c  39529  mapdvalc  39622  mapdval4N  39625  mapdordlem1a  39627  aks4d1p8  40075  prjsperref  40425  prjspeclsp  40431  elmzpcl  40528  mzpindd  40548  fphpd  40618  pw2f1ocnv  40839  islmodfg  40874  islssfg2  40876  isdomn3  41009  rp-isfinite6  41087  elmapintrab  41137  elinintrab  41138  relintab  41144  dfrtrcl5  41190  fsovrfovd  41570  ntrk1k3eqk13  41613  gneispace3  41696  k0004lem1  41710  pm13.192  41981  opelopab4  42124  ax6e2nd  42131  en3lplem2VD  42417  ax6e2ndVD  42481  ax6e2ndALT  42503  ssrabf  42617  limcrecl  43124  dvnprodlem2  43442  fourierdlem103  43704  fourierdlem104  43705  4an21  44713  sprvalpwn0  44887  pairreueq  44914  xpsnopab  45271  ismgmhm  45289  issubmgm  45295  submgmacs  45310  sgrp2sgrp  45374  opeliun2xp  45620  mpomptx2  45622  lindslinindsimp1  45750  lindslinindsimp2  45756  itsclc0b  46070  mo0sn  46113  iscnrm3lem3  46181  isthincd2  46271  thinccic  46294  alsconv  46446  aacllem  46457