Theorem anbi1i 636

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi2ci  637  bianbi  639  anandi  689  3an4anass  1122  3ioran  1123  4anpull2OLD  1384  an33rean  1515  an42ds  1520  19.26-3an  1905  sb3an  2120  eeeanv  2383  sbel2x  2506  rexcomf  3305  cbvreu  3408  rabeqi  3429  rabrabi  3434  rabrab  3439  ceqsex3v  3506  spc2ed  3559  rexrab  3657  reurab  3662  rmo3f  3695  reuind  3714  rmo3  3840  ssrab  3999  elin3  4106  inass  4127  rexin  4150  rexun  4197  dfun2  4218  inrab2  4265  rabun2  4272  reuun2  4273  undif4  4423  rexdifpr  4621  rexsns  4633  rexdifsn  4759  2ralunsn  4831  iuncom4  4965  iindif1  5040  iunxiun  5062  disjxun  5106  zfrep4  5252  inuni  5318  reusv2lem4  5370  reusv2  5372  otth2  5459  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  copsex2g  5472  copsex4g  5474  vopelopabsb  5510  rabxp  5706  opeliunxp  5725  opeliun2xp  5726  xpundir  5728  xpiundi  5729  xpiundir  5730  brinxp2  5737  copsex2gb  5793  cnvopab  6149  dminss  6161  imainss  6162  difxp  6173  cnvresima  6250  coundi  6267  resco  6270  imaco  6271  rnco  6272  rncoOLD  6273  coiun  6277  coi1  6285  coassOLD  6291  cnvpo  6314  xpco  6318  dfpo2  6325  frpoind  6371  dffun2  6576  fncnv  6643  imadif  6654  mptun  6715  ffrnb  6754  dff1o2  6860  dff1o3  6861  brprcneu  6906  brprcneuALT  6907  fvun2  7008  eqfnfv3  7062  respreima  7097  f1ompt  7143  f1ossf1o  7161  fsn  7168  fmptsng  7204  fmptsnd  7205  tpres  7238  abrexco  7279  imaiun  7280  f1mpt  7296  dff1o6  7314  riotarab  7450  oprabidw  7482  oprabid  7483  dfoprab2  7509  oprab4  7537  mpomptx  7564  mpt3mpt  7717  elpwpwel  7813  elxp4  7968  elxp5  7969  ffoss  7992  f11o  7993  opabex3d  8011  opabex3rd  8012  opabex3  8013  abexssex  8016  elxp7  8070  dfopab2  8098  dfoprab3s  8099  f1od2  8145  fsplit  8165  frxp  8175  xporderlem  8176  frpoins3xp3g  8195  soseq  8213  suppssov1  8252  suppssov2  8253  suppssfv  8257  brtpos2  8287  tpostpos  8301  tposmpo  8318  dfrecs3  8418  oarec  8608  oeeu  8650  eldifsucnn  8711  naddasslem1  8742  mapsncnv  8959  dfixp  8965  domen  9026  xpsnen  9118  xpcomco  9124  xpassen  9128  sbthlem9  9152  frfi  9314  marypha2lem2  9465  brttrcl2  9752  epfrs  9769  tcsni  9779  frind  9791  cp  9991  dfac5lem1  10241  dfac5lem2  10242  dfac5lem5  10245  kmlem3  10270  dfackm  10284  cfval2  10377  cflim3  10379  cfss  10382  cfslb  10383  zfcndrep  10738  eltsk2g  10875  ltexpi  11026  recmulnq  11088  ltexprlem4  11163  addsrpr  11199  mulsrpr  11200  addcnsr  11259  mulcnsr  11260  ltresr  11264  axrrecex  11287  elnnz  12743  elnn0z  12746  fnn0ind  12838  rexuz2  13066  rexrp  13183  elixx3g  13529  elfz2  13686  elfzuzb  13690  fznn  13766  elfz2nn0  13792  fznn0  13793  4fvwrd4  13822  preduz  13824  elfzo2  13836  fzind2  13963  hashgt23el  14610  hashf1lem1  14641  hashf1lem2  14642  fz1isolem  14647  s4f1o  15112  wwlktovfo  15154  fsum2dlem  15980  modfsummod  16005  prodeq1i  16129  sinltx  16401  divalglem10  16616  divalgb  16618  coprmproddvdslem  16881  isprm2  16901  infpn2  17135  prdsle  17683  prdsless  17684  prdsleval  17698  imasleval  17763  xpscf  17787  dfiso2  17997  oppcsect  18003  elhoma  18257  ispos2  18539  lubeldm  18575  glbeldm  18588  tosso  18641  ismgmhm  18935  issubmgm  18941  submgmacs  18956  ismhm  19030  issubm  19048  submacs  19073  issubg  19386  issubg3  19405  gaorb  19572  pmtrrn2  19725  efgcpbllema  20019  efgcpbllemb  20020  frgpuplem  20037  imasabl  20141  subgdmdprd  20301  dprd2d2  20311  omndmul2  20398  dfring3  20569  dfrhm2  20755  isrhm0  20757  opprnzrb  20823  issubrg  20874  isdomn3  21017  drngprop  21049  drngid2  21061  opprdrng  21072  isabv  21119  isorng  21169  islss  21260  islbs  21402  lsmspsn  21410  isobs  22081  islinds  22170  lindsenlbs  22212  isassa  22219  aspval2  22261  ltbval  22407  opsrle  22411  opsrtoslem1  22419  fvmptnn04if  23222  ntreq0  23450  restntr  23555  cnnei  23655  hausnei2  23726  cmpcov2  23763  cmpsub  23773  uncmp  23776  cmpfi  23781  llyi  23848  dissnlocfin  23903  iskgen3  23923  1stckgenlem  23927  ptpjpre1  23945  txcnpi  23982  txtube  24014  hausdiag  24019  txlm  24022  txkgen  24026  cfinfil  24267  csdfil  24268  supfil  24269  fin1aufil  24306  elflim2  24338  hauspwpwf1  24361  txflf  24380  isfcls  24383  alexsubALTlem3  24423  alexsubALT  24425  cnextcn  24441  istmd  24448  istgp  24451  tgphaus  24491  qustgplem  24495  istrg  24538  istdrg  24540  istlm  24559  blres  24805  isms2  24824  metrest  24898  metuel2  24939  restmetu  24944  isngp  24970  isnlm  25049  elii1  25311  isclmp  25473  iscvsp  25504  isncvsngp  25525  iscph  25546  cfilucfil3  25696  isbn  25714  limcrcl  26249  ig1pval3  26551  plydivex  26673  ellogdm  27024  cubic  27234  dmarea  27342  vmasum  27600  lgsquadlem2  27765  elno3  28069  lenlts  28166  madeval2  28276  elnnzs  28844  istrkg3ld  28980  legov  29105  ltgov  29117  colinearalg  29545  axeuclid  29598  axcontlem2  29600  axcontlem5  29603  nbgrel  29978  nbupgrres  30002  nbusgredgeu0  30006  nb3grprlem2  30019  nb3grpr2  30021  nb3gr2nb  30022  cplgr3v  30073  finsumvtxdg2ssteplem3  30185  wlkonprop  30294  upgrtrls  30341  upgristrl  30342  wksonproplem  30344  usgr2pth0  30408  wwlksnext  30539  wwlksnextsurj  30546  wwlksnfi  30552  wspthsnwspthsnon  30562  wpthswwlks2on  30610  rusgrnumwwlkl1  30617  erclwwlkref  30668  isclwwlknx  30684  clwwlknwwlksn  30686  clwwlkel  30694  erclwwlknref  30717  clwlknf1oclwwlkn  30732  clwwlknonel  30743  clwwlknon1  30745  clwwlknon2x  30751  clwwlkvbij  30761  iseupthf1o  30860  2pthfrgrrn  30940  fusgr2wsp2nb  30992  numclwwlk1lem2f1  31015  numclwwlkovh  31031  numclwlk2lem2f1o  31037  frgrregord013  31053  avril1  31121  islno  31412  h2hlm  31639  hcau  31843  hhsssh2  31929  dfch2  32066  elcnop  32516  ellnop  32517  elhmop  32532  elcnfn  32541  ellnfn  32542  dmadjss  32546  adjeu  32548  adjval  32549  hhcno  32563  hhcnf  32564  eleigvec  32616  isst  32872  ishst  32873  cvnbtwn3  32947  cvnbtwn4  32948  chirredi  33053  sumdmdii  33074  an52ds  33151  an62ds  33152  an72ds  33153  an82ds  33154  or3di  33156  rexunirn  33187  rmoun  33189  dmrab  33192  difrab2  33193  iunin1f  33250  disjunsn  33286  opeldifid  33291  ofpreima  33357  mpomptxf  33369  fdifsupp  33375  1stpreima  33397  2ndpreima  33398  resf1o  33418  maprnin  33419  nndiffz1  33474  ismnt  33643  mgcval  33647  erler  33925  opprnsg  34112  1arithidom  34173  1arithufdlem4  34183  extdgfialglem1  34435  smatrcl  34539  ordtconnlem1  34667  isrrext  34743  sigaex  34853  sigaval  34854  omssubaddlem  35042  omssubadd  35043  eulerpartleme  35106  eulerpartlemt0  35112  eulerpartlemr  35117  eulerpartlemn  35124  probun  35162  ballotlemelo  35231  ballotlem2  35232  ballotlemfc0  35236  ballotlemfcc  35237  reprdifc  35367  bnj248  35442  bnj250  35443  bnj268  35451  bnj312  35454  bnj945  35515  bnj110  35599  bnj849  35666  bnj882  35667  bnj893  35669  bnj916  35674  bnj983  35692  bnj1040  35713  bnj1175  35745  fwfffunres  35829  cusgredgex  36104  cusgr3cyclex  36109  erdszelem1  36164  iscvm  36232  elmpst  36509  mpstrcl  36514  dfso3  36700  xpab  36706  coepr  36733  dfdm5  36752  dfrn5  36753  elima4  36755  fv1stcnv  36756  fv2ndcnv  36757  brpprod  36862  dfon3  36869  elfix  36880  dffix2  36882  elfuns  36892  brimg  36914  brapply  36915  lemsuccf  36918  funpartlem  36921  funpartfun  36922  brrestrict  36928  dfrecs2  36929  dfrdg4  36930  lineunray  37127  ellines  37132  rmoeqi  37191  reueqi  37193  itgeq12i  37210  finminlem  37321  fneval  37355  neibastop3  37365  eliminable-abelv  37996  bj-inrab  38055  coi1res  38199  cocnv2ss  38213  bj-axseprep  38260  bj-rest10  38279  bj-restpw  38283  bj-restuni  38288  bj-mpomptALT  38311  copsex2gd  38330  bj-imdirco  38379  icorempo  38542  isbasisrelowllem1  38546  isbasisrelowllem2  38547  relowlpssretop  38555  pibt2  38608  wl-ifp-ncond2  38656  wl-df3-3mintru2  38677  wl-2mintru1  38681  rabiun  38789  iundif1  38790  poimirlem4  38810  poimirlem25  38831  poimirlem26  38832  poimirlem29  38835  poimirlem30  38836  ismblfin  38847  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  itg2addnclem2  38858  itg2addnclem3  38859  itg2addnc  38860  ftc1anc  38887  negprop  38911  isbnd2  38983  bndss  38986  heibor1lem  39009  heibor1  39010  isrngohom  39165  isidl  39214  sbccom2lem  39322  anan  39433  eqbrb  39437  eqelb  39439  br1cnvinxp  39457  eldmqsres  39491  idinxpssinxp2  39522  moantr  39570  inxpxrn  39616  blockadjliftmap  39656  dfcoss3  39702  cocossss  39724  ressn2  39730  br1cossinidres  39737  br1cossincnvepres  39738  br1cossxrnidres  39739  br1cossxrncnvepres  39740  refrelcoss2  39752  symrelcoss2  39754  cosscnvssid5  39766  br1cossxrncnvssrres  39786  dfrefrel3  39794  dfcnvrefrel3  39809  cosselcnvrefrels2  39816  cosselcnvrefrels3  39817  cosselcnvrefrels4  39818  cosselcnvrefrels5  39819  dfsymrel3  39832  refsymrel2  39849  refsymrel3  39850  elrefsymrels3  39852  dftrrel3  39860  dfeqvrel2  39872  dfeqvrel3  39873  redundpbi1  39913  refrelredund3  39919  eldmqs1cossres  39942  dffunALTV2  39971  dffunALTV3  39972  dffunALTV4  39973  dffunALTV5  39974  dfdisjALTV  39996  dfdisjALTV2  39997  dfdisjALTV3  39998  dfdisjALTV4  39999  disjimdmqseq  40007  eldisjs3  40019  eldisjs4  40020  disjsuc  40057  prtlem70  40180  prtlem100  40182  prter2  40204  lsateln0  40318  islshpat  40340  lcvnbtwn3  40351  islfl  40383  ishlat1  40675  ishlat2  40676  cvrat4  40766  islvol5  40902  psubspset  41067  snatpsubN  41073  dalawlem13  41206  psubclsetN  41259  isltrn2N  41443  cdlemftr3  41888  dibelval3  42470  dicval2  42502  dicopelval2  42504  dicelval2N  42505  dihglb2  42665  islpolN  42806  lcfls1c  42859  mapdvalc  42952  mapdval4N  42955  mapdordlem1a  42957  aks4d1p8  43403  fimgmcyc  43864  prjsperref  43900  prjspeclsp  43906  elmzpcl  44003  mzpindd  44023  fphpd  44089  pw2f1ocnv  44310  islmodfg  44337  islssfg2  44339  dflim6  44527  onsucf1olem  44533  omge2  44561  tfsconcatlem  44599  tfsconcat0i  44608  rp-isfinite6  44780  minregex  44796  elmapintrab  44838  elinintrab  44839  relintab  44845  dfrtrcl5  44890  fsovrfovd  45270  ntrk1k3eqk13  45311  gneispace3  45394  k0004lem1  45408  pm13.192  45655  opelopab4  45794  ax6e2nd  45801  en3lplem2VD  46086  ax6e2ndVD  46150  ax6e2ndALT  46172  permaxrep  46260  iuneq1i  46374  ssrabf  46402  limcrecl  46914  dvnprodlem2  47230  fourierdlem103  47492  fourierdlem104  47493  4an21  48613  sprvalpwn0  48838  pairreueq  48865  dfvopnbgr2  49224  isubgredg  49237  xpsnopab  49528  sgrp2sgrp  49598  mpomptx2  49778  lindslinindsimp1  49900  lindslinindsimp2  49906  itsclc0b  50215  mo0sn  50258  coxp  50275  isnat3  50673  fucoisfunc  50818  fucoisfunc2lem2  50820  isthincd2  50903  thinccic  50937  2arwcatlem1  51064  setc1onsubc  51071  alsanmo  51334  ralsanmo  51335  alsralrex  51336  aacllem  51367