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  4anpull2  1362  an33rean  1485  an42ds  1491  19.26-3an  1873  sb3an  2086  eeeanv  2354  sbel2x  2478  rexcomf  3275  cbvreu  3391  rabeqi  3412  rabrabi  3418  rabrab  3423  ceqsex3v  3495  spc2ed  3555  rexrab  3654  reurab  3659  rmo3f  3692  reuind  3711  rmo3  3839  ssrab  4023  rexun  4148  elin3  4158  inass  4180  rexin  4202  dfun2  4222  inrab2  4269  rabun2  4276  reuun2  4277  undif4  4419  rexdifpr  4616  rexsns  4628  rexdifsn  4750  2ralunsn  4851  iuncom4  4955  iindif1  5030  iunxiun  5052  disjxun  5096  zfrep4  5238  inuni  5295  reusv2lem4  5346  reusv2  5348  otth2  5431  copsexgw  5438  copsexg  5439  copsex2g  5441  copsex4g  5443  vopelopabsb  5477  rabxp  5672  opeliunxp  5691  opeliun2xp  5692  xpundir  5694  xpiundi  5695  xpiundir  5696  brinxp2  5702  copsex2gb  5755  cnvopab  6094  dminss  6111  imainss  6112  difxp  6122  cnvresima  6188  coundi  6205  resco  6208  imaco  6209  rnco  6210  rncoOLD  6211  coiun  6215  coi1  6221  coass  6224  cnvpo  6245  xpco  6247  dfpo2  6254  frpoind  6300  dffun2  6502  fncnv  6565  imadif  6576  mptun  6638  ffrnb  6676  dff1o2  6779  dff1o3  6780  brprcneu  6824  brprcneuALT  6825  fvun2  6926  eqfnfv3  6978  respreima  7011  f1ompt  7056  f1ossf1o  7073  fsn  7080  fmptsng  7114  fmptsnd  7115  tpres  7147  abrexco  7190  imaiun  7191  f1mpt  7207  dff1o6  7221  imaeqsexvOLD  7309  riotarab  7357  oprabidw  7389  oprabid  7390  dfoprab2  7416  oprab4  7444  mpomptx  7471  elpwpwel  7712  elxp4  7864  elxp5  7865  ffoss  7890  f11o  7891  opabex3d  7909  opabex3rd  7910  opabex3  7911  abexssex  7914  elxp7  7968  dfopab2  7996  dfoprab3s  7997  fsplit  8059  frxp  8068  xporderlem  8069  frpoins3xp3g  8083  soseq  8101  suppssov1  8139  suppssov2  8140  suppssfv  8144  brtpos2  8174  tpostpos  8188  tposmpo  8205  dfrecs3  8304  oarec  8489  oeeu  8531  eldifsucnn  8592  naddasslem1  8622  mapsncnv  8831  dfixp  8837  domen  8898  xpsnen  8989  xpcomco  8995  xpassen  8999  sbthlem9  9023  frfi  9185  marypha2lem2  9339  brttrcl2  9623  epfrs  9640  tcsni  9650  frind  9662  cp  9803  dfac5lem1  10033  dfac5lem2  10034  dfac5lem5  10037  kmlem3  10063  dfackm  10077  cfval2  10170  cflim3  10172  cfss  10175  cfslb  10176  zfcndrep  10525  eltsk2g  10662  ltexpi  10813  recmulnq  10875  ltexprlem4  10950  addsrpr  10986  mulsrpr  10987  addcnsr  11046  mulcnsr  11047  ltresr  11051  axrrecex  11074  elnnz  12498  elnn0z  12501  fnn0ind  12591  rexuz2  12812  rexrp  12928  elixx3g  13274  elfz2  13430  elfzuzb  13434  fznn  13508  elfz2nn0  13534  fznn0  13535  4fvwrd4  13564  preduz  13566  elfzo2  13578  fzind2  13704  hashgt23el  14347  hashf1lem1  14378  hashf1lem2  14379  fz1isolem  14384  s4f1o  14841  wwlktovfo  14881  fsum2dlem  15693  modfsummod  15717  prodeq1i  15839  sinltx  16114  divalglem10  16329  divalgb  16331  coprmproddvdslem  16589  isprm2  16609  infpn2  16841  prdsle  17382  prdsless  17383  prdsleval  17397  imasleval  17462  xpscf  17486  dfiso2  17696  oppcsect  17702  elhoma  17956  ispos2  18238  lubeldm  18274  glbeldm  18287  tosso  18340  ismgmhm  18621  issubmgm  18627  submgmacs  18642  ismhm  18710  issubm  18728  submacs  18752  issubg  19056  issubg3  19074  gaorb  19236  pmtrrn2  19389  efgcpbllema  19683  efgcpbllemb  19684  frgpuplem  19701  imasabl  19805  subgdmdprd  19965  dprd2d2  19975  omndmul2  20062  dfrhm2  20410  opprnzrb  20454  issubrg  20504  isdomn3  20648  drngprop  20677  drngid2  20685  opprdrng  20697  isabv  20744  isorng  20794  islss  20885  islbs  21028  lsmspsn  21036  isobs  21675  islinds  21764  isassa  21811  aspval2  21854  ltbval  21998  opsrle  22002  opsrtoslem1  22010  fvmptnn04if  22793  ntreq0  23021  restntr  23126  cnnei  23226  hausnei2  23297  cmpcov2  23334  cmpsub  23344  uncmp  23347  cmpfi  23352  llyi  23418  dissnlocfin  23473  iskgen3  23493  1stckgenlem  23497  ptpjpre1  23515  txcnpi  23552  txtube  23584  hausdiag  23589  txlm  23592  txkgen  23596  cfinfil  23837  csdfil  23838  supfil  23839  fin1aufil  23876  elflim2  23908  hauspwpwf1  23931  txflf  23950  isfcls  23953  alexsubALTlem3  23993  alexsubALT  23995  cnextcn  24011  istmd  24018  istgp  24021  tgphaus  24061  qustgplem  24065  istrg  24108  istdrg  24110  istlm  24129  blres  24375  isms2  24394  metrest  24468  metuel2  24509  restmetu  24514  isngp  24540  isnlm  24619  elii1  24887  isclmp  25053  iscvsp  25084  isncvsngp  25105  iscph  25126  cfilucfil3  25276  isbn  25294  limcrcl  25831  ig1pval3  26139  plydivex  26261  ellogdm  26604  cubic  26815  dmarea  26923  vmasum  27183  lgsquadlem1  27347  lgsquadlem2  27348  elno3  27623  lenlts  27720  madeval2  27829  elnnzs  28397  istrkg3ld  28533  legov  28657  ltgov  28669  colinearalg  28983  axeuclid  29036  axcontlem2  29038  axcontlem5  29041  nbgrel  29413  nbupgrres  29437  nbusgredgeu0  29441  nb3grprlem2  29454  nb3grpr2  29456  nb3gr2nb  29457  cplgr3v  29508  finsumvtxdg2ssteplem3  29621  wlkonprop  29730  upgrtrls  29773  upgristrl  29774  wksonproplem  29776  usgr2pth0  29838  wwlksnext  29966  wwlksnextsurj  29973  wwlksnfi  29979  wspthsnwspthsnon  29989  wpthswwlks2on  30037  rusgrnumwwlkl1  30044  erclwwlkref  30095  isclwwlknx  30111  clwwlknwwlksn  30113  clwwlkel  30121  erclwwlknref  30144  clwlknf1oclwwlkn  30159  clwwlknonel  30170  clwwlknon1  30172  clwwlknon2x  30178  clwwlkvbij  30188  iseupthf1o  30277  2pthfrgrrn  30357  fusgr2wsp2nb  30409  numclwwlk1lem2f1  30432  numclwwlkovh  30448  numclwlk2lem2f1o  30454  frgrregord013  30470  avril1  30538  islno  30828  h2hlm  31055  hcau  31259  hhsssh2  31345  dfch2  31482  elcnop  31932  ellnop  31933  elhmop  31948  elcnfn  31957  ellnfn  31958  dmadjss  31962  adjeu  31964  adjval  31965  hhcno  31979  hhcnf  31980  eleigvec  32032  isst  32288  ishst  32289  cvnbtwn3  32363  cvnbtwn4  32364  chirredi  32469  sumdmdii  32490  an52ds  32525  an62ds  32526  an72ds  32527  an82ds  32528  or3di  32533  rexunirn  32566  rmoun  32568  dmrab  32571  difrab2  32572  iunin1f  32632  disjunsn  32669  opeldifid  32674  ofpreima  32743  mpomptxf  32757  fdifsupp  32764  1stpreima  32786  2ndpreima  32787  f1od2  32798  resf1o  32809  maprnin  32810  nndiffz1  32866  ismnt  33065  mgcval  33069  erler  33347  opprnsg  33565  1arithidom  33618  1arithufdlem4  33628  extdgfialglem1  33849  smatrcl  33953  ordtconnlem1  34081  isrrext  34157  sigaex  34267  sigaval  34268  omssubaddlem  34456  omssubadd  34457  eulerpartleme  34520  eulerpartlemt0  34526  eulerpartlemr  34531  eulerpartlemn  34538  probun  34576  ballotlemelo  34645  ballotlem2  34646  ballotlemfc0  34650  ballotlemfcc  34651  reprdifc  34784  bnj248  34856  bnj250  34857  bnj268  34865  bnj312  34868  bnj945  34929  bnj110  35014  bnj849  35081  bnj882  35082  bnj893  35084  bnj916  35089  bnj983  35107  bnj1040  35128  bnj1175  35160  cusgredgex  35316  cusgr3cyclex  35330  erdszelem1  35385  iscvm  35453  elmpst  35730  mpstrcl  35735  dfso3  35914  xpab  35920  coepr  35947  dfdm5  35967  dfrn5  35968  elima4  35970  fv1stcnv  35971  fv2ndcnv  35972  brpprod  36077  dfon3  36084  elfix  36095  dffix2  36097  elfuns  36107  brimg  36129  brapply  36130  lemsuccf  36133  funpartlem  36136  funpartfun  36137  brrestrict  36143  dfrecs2  36144  dfrdg4  36145  lineunray  36341  ellines  36346  rmoeqi  36381  reueqi  36383  itgeq12i  36400  finminlem  36512  fneval  36546  neibastop3  36556  eliminable-abelv  37070  bj-inrab  37128  bj-rest10  37293  bj-restpw  37297  bj-restuni  37302  bj-mpomptALT  37324  bj-imdirco  37395  icorempo  37556  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlpssretop  37569  pibt2  37622  wl-ifp-ncond2  37670  wl-df3-3mintru2  37691  wl-2mintru1  37695  rabiun  37794  iundif1  37795  lindsenlbs  37816  poimirlem4  37825  poimirlem25  37846  poimirlem26  37847  poimirlem29  37850  poimirlem30  37851  ismblfin  37862  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  itg2addnclem2  37873  itg2addnclem3  37874  itg2addnc  37875  ftc1anc  37902  isbnd2  37984  bndss  37987  heibor1lem  38010  heibor1  38011  isrngohom  38166  isidl  38215  sbccom2lem  38325  anan  38431  eqbrb  38435  eqelb  38437  br1cnvinxp  38454  eldmqsres  38486  idinxpssinxp2  38517  moantr  38557  inxpxrn  38603  blockadjliftmap  38633  dfcoss3  38677  cocossss  38699  ressn2  38705  br1cossinidres  38712  br1cossincnvepres  38713  br1cossxrnidres  38714  br1cossxrncnvepres  38715  refrelcoss2  38727  symrelcoss2  38729  cosscnvssid5  38741  br1cossxrncnvssrres  38761  dfrefrel3  38769  dfcnvrefrel3  38784  cosselcnvrefrels2  38791  cosselcnvrefrels3  38792  cosselcnvrefrels4  38793  cosselcnvrefrels5  38794  dfsymrel3  38807  refsymrel2  38824  refsymrel3  38825  elrefsymrels3  38827  dftrrel3  38835  dfeqvrel2  38847  dfeqvrel3  38848  redundpbi1  38888  refrelredund3  38894  eldmqs1cossres  38918  dffunALTV2  38947  dffunALTV3  38948  dffunALTV4  38949  dffunALTV5  38950  dfdisjALTV  38972  dfdisjALTV2  38973  dfdisjALTV3  38974  dfdisjALTV4  38975  eldisjs3  38983  eldisjs4  38984  disjsuc  39018  prtlem70  39117  prtlem100  39119  prter2  39141  lsateln0  39255  islshpat  39277  lcvnbtwn3  39288  islfl  39320  ishlat1  39612  ishlat2  39613  cvrat4  39703  islvol5  39839  psubspset  40004  snatpsubN  40010  dalawlem13  40143  psubclsetN  40196  isltrn2N  40380  cdlemftr3  40825  dibelval3  41407  dicval2  41439  dicopelval2  41441  dicelval2N  41442  dihglb2  41602  islpolN  41743  lcfls1c  41796  mapdvalc  41889  mapdval4N  41892  mapdordlem1a  41894  aks4d1p8  42341  fimgmcyc  42789  prjsperref  42849  prjspeclsp  42855  elmzpcl  42968  mzpindd  42988  fphpd  43058  pw2f1ocnv  43279  islmodfg  43311  islssfg2  43313  dflim6  43506  onsucf1olem  43512  omge2  43540  tfsconcatlem  43578  tfsconcat0i  43587  rp-isfinite6  43759  minregex  43775  elmapintrab  43817  elinintrab  43818  relintab  43824  dfrtrcl5  43870  fsovrfovd  44250  ntrk1k3eqk13  44291  gneispace3  44374  k0004lem1  44388  pm13.192  44651  opelopab4  44792  ax6e2nd  44799  en3lplem2VD  45084  ax6e2ndVD  45148  ax6e2ndALT  45170  permaxrep  45247  iuneq1i  45329  ssrabf  45358  limcrecl  45875  dvnprodlem2  46191  fourierdlem103  46453  fourierdlem104  46454  4an21  47516  sprvalpwn0  47729  pairreueq  47756  dfvopnbgr2  48099  isubgredg  48112  xpsnopab  48403  sgrp2sgrp  48474  mpomptx2  48581  lindslinindsimp1  48703  lindslinindsimp2  48709  itsclc0b  49018  mo0sn  49061  coxp  49078  isthincd2  49682  thinccic  49716  2arwcatlem1  49840  setc1onsubc  49847  alsconv  50035  aacllem  50046