Theorem anbi1i 633

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi2ci  634  bianbi  636  anandi  686  3an4anass  1117  3ioran  1118  4anpull2  1375  an33rean  1504  an42ds  1510  19.26-3an  1892  sb3an  2114  eeeanv  2381  sbel2x  2505  rexcomf  3301  cbvreu  3406  rabeqi  3427  rabrabi  3433  rabrab  3438  ceqsex3v  3506  spc2ed  3560  rexrab  3659  reurab  3664  rmo3f  3697  reuind  3716  rmo3  3842  ssrab  4024  rexun  4148  elin3  4158  inass  4179  rexin  4202  dfun2  4222  inrab2  4269  rabun2  4276  reuun2  4277  undif4  4421  rexdifpr  4618  rexsns  4630  rexdifsn  4754  2ralunsn  4853  iuncom4  4958  iindif1  5032  iunxiun  5054  disjxun  5098  zfrep4  5243  inuni  5306  reusv2lem4  5358  reusv2  5360  otth2  5451  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  copsex2g  5462  copsex4g  5464  vopelopabsb  5499  rabxp  5695  opeliunxp  5714  opeliun2xp  5715  xpundir  5717  xpiundi  5718  xpiundir  5719  brinxp2  5725  copsex2gb  5779  cnvopab  6124  dminss  6138  imainss  6139  difxp  6149  cnvresima  6217  coundi  6234  resco  6237  imaco  6238  rnco  6239  rncoOLD  6240  coiun  6244  coi1  6250  coass  6253  cnvpo  6274  xpco  6276  dfpo2  6283  frpoind  6329  dffun2  6531  fncnv  6594  imadif  6605  mptun  6667  ffrnb  6706  dff1o2  6812  dff1o3  6813  brprcneu  6857  brprcneuALT  6858  fvun2  6959  eqfnfv3  7013  respreima  7047  f1ompt  7092  f1ossf1o  7110  fsn  7117  fmptsng  7152  fmptsnd  7153  tpres  7185  abrexco  7228  imaiun  7229  f1mpt  7245  dff1o6  7259  imaeqsexvOLD  7347  riotarab  7395  oprabidw  7427  oprabid  7428  dfoprab2  7454  oprab4  7482  mpomptx  7509  elpwpwel  7750  elxp4  7903  elxp5  7904  ffoss  7927  f11o  7928  opabex3d  7946  opabex3rd  7947  opabex3  7948  abexssex  7951  elxp7  8005  dfopab2  8033  dfoprab3s  8034  fsplit  8096  frxp  8106  xporderlem  8107  frpoins3xp3g  8121  soseq  8139  suppssov1  8177  suppssov2  8178  suppssfv  8182  brtpos2  8212  tpostpos  8226  tposmpo  8243  dfrecs3  8343  oarec  8531  oeeu  8573  eldifsucnn  8634  naddasslem1  8665  mapsncnv  8875  dfixp  8881  domen  8942  xpsnen  9033  xpcomco  9039  xpassen  9043  sbthlem9  9067  frfi  9229  marypha2lem2  9382  brttrcl2  9669  epfrs  9686  tcsni  9696  frind  9708  cp  9849  dfac5lem1  10079  dfac5lem2  10080  dfac5lem5  10083  kmlem3  10109  dfackm  10123  cfval2  10217  cflim3  10219  cfss  10222  cfslb  10223  zfcndrep  10572  eltsk2g  10709  ltexpi  10860  recmulnq  10922  ltexprlem4  10997  addsrpr  11033  mulsrpr  11034  addcnsr  11093  mulcnsr  11094  ltresr  11098  axrrecex  11121  elnnz  12578  elnn0z  12581  fnn0ind  12672  rexuz2  12900  rexrp  13016  elixx3g  13362  elfz2  13519  elfzuzb  13523  fznn  13597  elfz2nn0  13623  fznn0  13624  4fvwrd4  13653  preduz  13655  elfzo2  13667  fzind2  13794  hashgt23el  14437  hashf1lem1  14468  hashf1lem2  14469  fz1isolem  14474  s4f1o  14931  wwlktovfo  14971  fsum2dlem  15797  modfsummod  15822  prodeq1i  15946  sinltx  16221  divalglem10  16436  divalgb  16438  coprmproddvdslem  16696  isprm2  16716  infpn2  16949  prdsle  17491  prdsless  17492  prdsleval  17506  imasleval  17571  xpscf  17595  dfiso2  17805  oppcsect  17811  elhoma  18065  ispos2  18347  lubeldm  18383  glbeldm  18396  tosso  18449  ismgmhm  18730  issubmgm  18736  submgmacs  18751  ismhm  18819  issubm  18837  submacs  18861  issubg  19168  issubg3  19186  gaorb  19347  pmtrrn2  19500  efgcpbllema  19794  efgcpbllemb  19795  frgpuplem  19812  imasabl  19916  subgdmdprd  20076  dprd2d2  20086  omndmul2  20173  dfrhm2  20523  opprnzrb  20571  issubrg  20621  isdomn3  20765  drngprop  20794  drngid2  20802  opprdrng  20814  isabv  20860  isorng  20910  islss  21001  islbs  21143  lsmspsn  21151  isobs  21772  islinds  21861  isassa  21908  aspval2  21950  ltbval  22096  opsrle  22100  opsrtoslem1  22108  fvmptnn04if  22909  ntreq0  23137  restntr  23242  cnnei  23342  hausnei2  23413  cmpcov2  23450  cmpsub  23460  uncmp  23463  cmpfi  23468  llyi  23534  dissnlocfin  23589  iskgen3  23609  1stckgenlem  23613  ptpjpre1  23631  txcnpi  23668  txtube  23700  hausdiag  23705  txlm  23708  txkgen  23712  cfinfil  23953  csdfil  23954  supfil  23955  fin1aufil  23992  elflim2  24024  hauspwpwf1  24047  txflf  24066  isfcls  24069  alexsubALTlem3  24109  alexsubALT  24111  cnextcn  24127  istmd  24134  istgp  24137  tgphaus  24177  qustgplem  24181  istrg  24224  istdrg  24226  istlm  24245  blres  24491  isms2  24510  metrest  24584  metuel2  24625  restmetu  24630  isngp  24656  isnlm  24735  elii1  24997  isclmp  25159  iscvsp  25190  isncvsngp  25211  iscph  25232  cfilucfil3  25382  isbn  25400  limcrcl  25936  ig1pval3  26238  plydivex  26361  ellogdm  26704  cubic  26914  dmarea  27022  vmasum  27280  lgsquadlem1  27444  lgsquadlem2  27445  elno3  27719  lenlts  27816  madeval2  27926  elnnzs  28494  istrkg3ld  28630  legov  28754  ltgov  28766  colinearalg  29111  axeuclid  29164  axcontlem2  29166  axcontlem5  29169  nbgrel  29541  nbupgrres  29565  nbusgredgeu0  29569  nb3grprlem2  29582  nb3grpr2  29584  nb3gr2nb  29585  cplgr3v  29636  finsumvtxdg2ssteplem3  29748  wlkonprop  29857  upgrtrls  29900  upgristrl  29901  wksonproplem  29903  usgr2pth0  29965  wwlksnext  30093  wwlksnextsurj  30100  wwlksnfi  30106  wspthsnwspthsnon  30116  wpthswwlks2on  30164  rusgrnumwwlkl1  30171  erclwwlkref  30222  isclwwlknx  30238  clwwlknwwlksn  30240  clwwlkel  30248  erclwwlknref  30271  clwlknf1oclwwlkn  30286  clwwlknonel  30297  clwwlknon1  30299  clwwlknon2x  30305  clwwlkvbij  30315  iseupthf1o  30404  2pthfrgrrn  30484  fusgr2wsp2nb  30536  numclwwlk1lem2f1  30559  numclwwlkovh  30575  numclwlk2lem2f1o  30581  frgrregord013  30597  avril1  30665  islno  30956  h2hlm  31183  hcau  31387  hhsssh2  31473  dfch2  31610  elcnop  32060  ellnop  32061  elhmop  32076  elcnfn  32085  ellnfn  32086  dmadjss  32090  adjeu  32092  adjval  32093  hhcno  32107  hhcnf  32108  eleigvec  32160  isst  32416  ishst  32417  cvnbtwn3  32491  cvnbtwn4  32492  chirredi  32597  sumdmdii  32618  an52ds  32653  an62ds  32654  an72ds  32655  an82ds  32656  or3di  32659  rexunirn  32691  rmoun  32693  dmrab  32696  difrab2  32697  iunin1f  32757  disjunsn  32794  opeldifid  32799  ofpreima  32867  mpomptxf  32880  fdifsupp  32887  1stpreima  32909  2ndpreima  32910  f1od2  32921  resf1o  32932  maprnin  32933  nndiffz1  32988  ismnt  33161  mgcval  33165  erler  33446  opprnsg  33672  1arithidom  33733  1arithufdlem4  33743  extdgfialglem1  33989  smatrcl  34093  ordtconnlem1  34221  isrrext  34297  sigaex  34407  sigaval  34408  omssubaddlem  34596  omssubadd  34597  eulerpartleme  34660  eulerpartlemt0  34666  eulerpartlemr  34671  eulerpartlemn  34678  probun  34716  ballotlemelo  34785  ballotlem2  34786  ballotlemfc0  34790  ballotlemfcc  34791  reprdifc  34921  bnj248  34996  bnj250  34997  bnj268  35005  bnj312  35008  bnj945  35069  bnj110  35153  bnj849  35220  bnj882  35221  bnj893  35223  bnj916  35228  bnj983  35246  bnj1040  35267  bnj1175  35299  cusgredgex  35472  cusgr3cyclex  35486  erdszelem1  35541  iscvm  35609  elmpst  35886  mpstrcl  35891  dfso3  36070  xpab  36076  coepr  36103  dfdm5  36123  dfrn5  36124  elima4  36126  fv1stcnv  36127  fv2ndcnv  36128  brpprod  36233  dfon3  36240  elfix  36251  dffix2  36253  elfuns  36263  brimg  36285  brapply  36286  lemsuccf  36289  funpartlem  36292  funpartfun  36293  brrestrict  36299  dfrecs2  36300  dfrdg4  36301  lineunray  36497  ellines  36502  rmoeqi  36547  reueqi  36549  itgeq12i  36566  finminlem  36678  fneval  36712  neibastop3  36722  eliminable-abelv  37354  bj-inrab  37412  bj-axseprep  37559  bj-rest10  37578  bj-restpw  37582  bj-restuni  37587  bj-mpomptALT  37609  copsex2gd  37630  bj-imdirco  37682  icorempo  37845  isbasisrelowllem1  37849  isbasisrelowllem2  37850  relowlpssretop  37858  pibt2  37911  wl-ifp-ncond2  37959  wl-df3-3mintru2  37980  wl-2mintru1  37984  rabiun  38092  iundif1  38093  lindsenlbs  38114  poimirlem4  38123  poimirlem25  38144  poimirlem26  38145  poimirlem29  38148  poimirlem30  38149  ismblfin  38160  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  itg2addnclem2  38171  itg2addnclem3  38172  itg2addnc  38173  ftc1anc  38200  isbnd2  38282  bndss  38285  heibor1lem  38308  heibor1  38309  isrngohom  38464  isidl  38513  sbccom2lem  38623  anan  38734  eqbrb  38738  eqelb  38740  br1cnvinxp  38758  eldmqsres  38792  idinxpssinxp2  38823  moantr  38871  inxpxrn  38917  blockadjliftmap  38957  dfcoss3  39003  cocossss  39025  ressn2  39031  br1cossinidres  39038  br1cossincnvepres  39039  br1cossxrnidres  39040  br1cossxrncnvepres  39041  refrelcoss2  39053  symrelcoss2  39055  cosscnvssid5  39067  br1cossxrncnvssrres  39087  dfrefrel3  39095  dfcnvrefrel3  39110  cosselcnvrefrels2  39117  cosselcnvrefrels3  39118  cosselcnvrefrels4  39119  cosselcnvrefrels5  39120  dfsymrel3  39133  refsymrel2  39150  refsymrel3  39151  elrefsymrels3  39153  dftrrel3  39161  dfeqvrel2  39173  dfeqvrel3  39174  redundpbi1  39214  refrelredund3  39220  eldmqs1cossres  39243  dffunALTV2  39272  dffunALTV3  39273  dffunALTV4  39274  dffunALTV5  39275  dfdisjALTV  39297  dfdisjALTV2  39298  dfdisjALTV3  39299  dfdisjALTV4  39300  disjimdmqseq  39308  eldisjs3  39320  eldisjs4  39321  disjsuc  39358  prtlem70  39481  prtlem100  39483  prter2  39505  lsateln0  39619  islshpat  39641  lcvnbtwn3  39652  islfl  39684  ishlat1  39976  ishlat2  39977  cvrat4  40067  islvol5  40203  psubspset  40368  snatpsubN  40374  dalawlem13  40507  psubclsetN  40560  isltrn2N  40744  cdlemftr3  41189  dibelval3  41771  dicval2  41803  dicopelval2  41805  dicelval2N  41806  dihglb2  41966  islpolN  42107  lcfls1c  42160  mapdvalc  42253  mapdval4N  42256  mapdordlem1a  42258  aks4d1p8  42704  fimgmcyc  43152  prjsperref  43188  prjspeclsp  43194  elmzpcl  43307  mzpindd  43327  fphpd  43393  pw2f1ocnv  43614  islmodfg  43646  islssfg2  43648  dflim6  43841  onsucf1olem  43847  omge2  43875  tfsconcatlem  43913  tfsconcat0i  43922  rp-isfinite6  44094  minregex  44110  elmapintrab  44152  elinintrab  44153  relintab  44159  dfrtrcl5  44205  fsovrfovd  44585  ntrk1k3eqk13  44626  gneispace3  44709  k0004lem1  44723  pm13.192  44986  opelopab4  45127  ax6e2nd  45134  en3lplem2VD  45419  ax6e2ndVD  45483  ax6e2ndALT  45505  permaxrep  45582  iuneq1i  45664  ssrabf  45692  limcrecl  46205  dvnprodlem2  46521  fourierdlem103  46783  fourierdlem104  46784  4an21  47864  sprvalpwn0  48089  pairreueq  48116  dfvopnbgr2  48475  isubgredg  48488  xpsnopab  48779  sgrp2sgrp  48850  mpomptx2  48957  lindslinindsimp1  49079  lindslinindsimp2  49085  itsclc0b  49394  mo0sn  49437  coxp  49454  isthincd2  50058  thinccic  50092  2arwcatlem1  50216  setc1onsubc  50223  alsconv  50411  aacllem  50422