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  1383  an33rean  1514  an42ds  1519  19.26-3an  1904  sb3an  2119  eeeanv  2382  sbel2x  2506  rexcomf  3304  cbvreu  3407  rabeqi  3428  rabrabi  3433  rabrab  3438  ceqsex3v  3505  spc2ed  3558  rexrab  3656  reurab  3661  rmo3f  3694  reuind  3713  rmo3  3839  ssrab  3998  elin3  4105  inass  4126  rexin  4149  rexun  4196  dfun2  4217  inrab2  4264  rabun2  4271  reuun2  4272  undif4  4422  rexdifpr  4619  rexsns  4631  rexdifsn  4756  2ralunsn  4828  iuncom4  4962  iindif1  5037  iunxiun  5059  disjxun  5103  zfrep4  5248  inuni  5314  reusv2lem4  5366  reusv2  5368  otth2  5455  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  cotsexgw  5466  copsex2g  5468  copsex4g  5470  vopelopabsb  5506  rabxp  5702  opeliunxp  5721  opeliun2xp  5722  xpundir  5724  xpiundi  5725  xpiundir  5726  brinxp2  5733  copsex2gb  5788  cnvopab  6136  dminss  6148  imainss  6149  difxp  6160  cnvresima  6237  coundi  6254  resco  6257  imaco  6258  rnco  6259  rncoOLD  6260  coiun  6264  coi1  6270  coass  6273  cnvpo  6296  xpco  6298  dfpo2  6305  frpoind  6351  dffun2  6556  fncnv  6621  imadif  6632  mptun  6693  ffrnb  6732  dff1o2  6838  dff1o3  6839  brprcneu  6883  brprcneuALT  6884  fvun2  6985  eqfnfv3  7039  respreima  7073  f1ompt  7119  f1ossf1o  7137  fsn  7144  fmptsng  7180  fmptsnd  7181  tpres  7214  abrexco  7255  imaiun  7256  f1mpt  7272  dff1o6  7290  riotarab  7426  oprabidw  7458  oprabid  7459  dfoprab2  7485  oprab4  7513  mpomptx  7540  mpt3mpt  7692  elpwpwel  7788  elxp4  7941  elxp5  7942  ffoss  7965  f11o  7966  opabex3d  7984  opabex3rd  7985  opabex3  7986  abexssex  7989  elxp7  8043  dfopab2  8071  dfoprab3s  8072  f1od2  8118  fsplit  8138  frxp  8148  xporderlem  8149  frpoins3xp3g  8168  soseq  8186  suppssov1  8225  suppssov2  8226  suppssfv  8230  brtpos2  8260  tpostpos  8274  tposmpo  8291  dfrecs3  8391  oarec  8581  oeeu  8623  eldifsucnn  8684  naddasslem1  8715  mapsncnv  8932  dfixp  8938  domen  8999  xpsnen  9091  xpcomco  9097  xpassen  9101  sbthlem9  9125  frfi  9287  marypha2lem2  9438  brttrcl2  9725  epfrs  9742  tcsni  9752  frind  9764  cp  9964  dfac5lem1  10212  dfac5lem2  10213  dfac5lem5  10216  kmlem3  10241  dfackm  10255  cfval2  10348  cflim3  10350  cfss  10353  cfslb  10354  zfcndrep  10709  eltsk2g  10846  ltexpi  10997  recmulnq  11059  ltexprlem4  11134  addsrpr  11170  mulsrpr  11171  addcnsr  11230  mulcnsr  11231  ltresr  11235  axrrecex  11258  elnnz  12713  elnn0z  12716  fnn0ind  12808  rexuz2  13036  rexrp  13153  elixx3g  13499  elfz2  13656  elfzuzb  13660  fznn  13736  elfz2nn0  13762  fznn0  13763  4fvwrd4  13792  preduz  13794  elfzo2  13806  fzind2  13933  hashgt23el  14579  hashf1lem1  14610  hashf1lem2  14611  fz1isolem  14616  s4f1o  15081  wwlktovfo  15123  fsum2dlem  15948  modfsummod  15973  prodeq1i  16097  sinltx  16369  divalglem10  16584  divalgb  16586  coprmproddvdslem  16849  isprm2  16869  infpn2  17103  prdsle  17645  prdsless  17646  prdsleval  17660  imasleval  17725  xpscf  17749  dfiso2  17959  oppcsect  17965  elhoma  18219  ispos2  18501  lubeldm  18537  glbeldm  18550  tosso  18603  ismgmhm  18897  issubmgm  18903  submgmacs  18918  ismhm  18992  issubm  19010  submacs  19035  issubg  19348  issubg3  19367  gaorb  19533  pmtrrn2  19686  efgcpbllema  19980  efgcpbllemb  19981  frgpuplem  19998  imasabl  20102  subgdmdprd  20262  dprd2d2  20272  omndmul2  20359  dfring3  20530  dfrhm2  20716  isrhm0  20718  opprnzrb  20784  issubrg  20835  isdomn3  20978  drngprop  21010  drngid2  21022  opprdrng  21033  isabv  21080  isorng  21130  islss  21221  islbs  21363  lsmspsn  21371  isobs  22038  islinds  22127  lindsenlbs  22169  isassa  22176  aspval2  22218  ltbval  22364  opsrle  22368  opsrtoslem1  22376  fvmptnn04if  23179  ntreq0  23407  restntr  23512  cnnei  23612  hausnei2  23683  cmpcov2  23720  cmpsub  23730  uncmp  23733  cmpfi  23738  llyi  23805  dissnlocfin  23860  iskgen3  23880  1stckgenlem  23884  ptpjpre1  23902  txcnpi  23939  txtube  23971  hausdiag  23976  txlm  23979  txkgen  23983  cfinfil  24224  csdfil  24225  supfil  24226  fin1aufil  24263  elflim2  24295  hauspwpwf1  24318  txflf  24337  isfcls  24340  alexsubALTlem3  24380  alexsubALT  24382  cnextcn  24398  istmd  24405  istgp  24408  tgphaus  24448  qustgplem  24452  istrg  24495  istdrg  24497  istlm  24516  blres  24762  isms2  24781  metrest  24855  metuel2  24896  restmetu  24901  isngp  24927  isnlm  25006  elii1  25268  isclmp  25430  iscvsp  25461  isncvsngp  25482  iscph  25503  cfilucfil3  25653  isbn  25671  limcrcl  26206  ig1pval3  26508  plydivex  26630  ellogdm  26979  cubic  27189  dmarea  27297  vmasum  27555  lgsquadlem2  27720  elno3  28024  lenlts  28121  madeval2  28231  elnnzs  28799  istrkg3ld  28935  legov  29060  ltgov  29072  colinearalg  29500  axeuclid  29553  axcontlem2  29555  axcontlem5  29558  nbgrel  29933  nbupgrres  29957  nbusgredgeu0  29961  nb3grprlem2  29974  nb3grpr2  29976  nb3gr2nb  29977  cplgr3v  30028  finsumvtxdg2ssteplem3  30140  wlkonprop  30249  upgrtrls  30296  upgristrl  30297  wksonproplem  30299  usgr2pth0  30363  wwlksnext  30494  wwlksnextsurj  30501  wwlksnfi  30507  wspthsnwspthsnon  30517  wpthswwlks2on  30565  rusgrnumwwlkl1  30572  erclwwlkref  30623  isclwwlknx  30639  clwwlknwwlksn  30641  clwwlkel  30649  erclwwlknref  30672  clwlknf1oclwwlkn  30687  clwwlknonel  30698  clwwlknon1  30700  clwwlknon2x  30706  clwwlkvbij  30716  iseupthf1o  30815  2pthfrgrrn  30895  fusgr2wsp2nb  30947  numclwwlk1lem2f1  30970  numclwwlkovh  30986  numclwlk2lem2f1o  30992  frgrregord013  31008  avril1  31076  islno  31367  h2hlm  31594  hcau  31798  hhsssh2  31884  dfch2  32021  elcnop  32471  ellnop  32472  elhmop  32487  elcnfn  32496  ellnfn  32497  dmadjss  32501  adjeu  32503  adjval  32504  hhcno  32518  hhcnf  32519  eleigvec  32571  isst  32827  ishst  32828  cvnbtwn3  32902  cvnbtwn4  32903  chirredi  33008  sumdmdii  33029  an52ds  33106  an62ds  33107  an72ds  33108  an82ds  33109  or3di  33111  rexunirn  33142  rmoun  33144  dmrab  33147  difrab2  33148  iunin1f  33206  disjunsn  33242  opeldifid  33247  ofpreima  33313  mpomptxf  33326  fdifsupp  33332  1stpreima  33354  2ndpreima  33355  resf1o  33375  maprnin  33376  nndiffz1  33431  ismnt  33597  mgcval  33601  erler  33879  opprnsg  34061  1arithidom  34122  1arithufdlem4  34132  extdgfialglem1  34377  smatrcl  34481  ordtconnlem1  34609  isrrext  34685  sigaex  34795  sigaval  34796  omssubaddlem  34984  omssubadd  34985  eulerpartleme  35048  eulerpartlemt0  35054  eulerpartlemr  35059  eulerpartlemn  35066  probun  35104  ballotlemelo  35173  ballotlem2  35174  ballotlemfc0  35178  ballotlemfcc  35179  reprdifc  35309  bnj248  35384  bnj250  35385  bnj268  35393  bnj312  35396  bnj945  35457  bnj110  35541  bnj849  35608  bnj882  35609  bnj893  35611  bnj916  35616  bnj983  35634  bnj1040  35655  bnj1175  35687  fwfffunres  35771  cusgredgex  36017  cusgr3cyclex  36022  erdszelem1  36077  iscvm  36145  elmpst  36422  mpstrcl  36427  dfso3  36612  xpab  36618  coepr  36645  dfdm5  36664  dfrn5  36665  elima4  36667  fv1stcnv  36668  fv2ndcnv  36669  brpprod  36774  dfon3  36781  elfix  36792  dffix2  36794  elfuns  36804  brimg  36826  brapply  36827  lemsuccf  36830  funpartlem  36833  funpartfun  36834  brrestrict  36840  dfrecs2  36841  dfrdg4  36842  lineunray  37039  ellines  37044  rmoeqi  37103  reueqi  37105  itgeq12i  37122  finminlem  37233  fneval  37267  neibastop3  37277  eliminable-abelv  37908  bj-inrab  37967  coi1res  38099  bj-axseprep  38129  bj-rest10  38148  bj-restpw  38152  bj-restuni  38157  bj-mpomptALT  38180  copsex2gd  38199  bj-imdirco  38251  icorempo  38414  isbasisrelowllem1  38418  isbasisrelowllem2  38419  relowlpssretop  38427  pibt2  38480  wl-ifp-ncond2  38528  wl-df3-3mintru2  38549  wl-2mintru1  38553  rabiun  38661  iundif1  38662  poimirlem4  38682  poimirlem25  38703  poimirlem26  38704  poimirlem29  38707  poimirlem30  38708  ismblfin  38719  ovoliunnfl  38720  voliunnfl  38722  volsupnfl  38723  itg2addnclem2  38730  itg2addnclem3  38731  itg2addnc  38732  ftc1anc  38759  negprop  38783  isbnd2  38857  bndss  38860  heibor1lem  38883  heibor1  38884  isrngohom  39039  isidl  39088  sbccom2lem  39196  anan  39307  eqbrb  39311  eqelb  39313  br1cnvinxp  39331  eldmqsres  39365  idinxpssinxp2  39396  moantr  39444  inxpxrn  39490  blockadjliftmap  39530  dfcoss3  39576  cocossss  39598  ressn2  39604  br1cossinidres  39611  br1cossincnvepres  39612  br1cossxrnidres  39613  br1cossxrncnvepres  39614  refrelcoss2  39626  symrelcoss2  39628  cosscnvssid5  39640  br1cossxrncnvssrres  39660  dfrefrel3  39668  dfcnvrefrel3  39683  cosselcnvrefrels2  39690  cosselcnvrefrels3  39691  cosselcnvrefrels4  39692  cosselcnvrefrels5  39693  dfsymrel3  39706  refsymrel2  39723  refsymrel3  39724  elrefsymrels3  39726  dftrrel3  39734  dfeqvrel2  39746  dfeqvrel3  39747  redundpbi1  39787  refrelredund3  39793  eldmqs1cossres  39816  dffunALTV2  39845  dffunALTV3  39846  dffunALTV4  39847  dffunALTV5  39848  dfdisjALTV  39870  dfdisjALTV2  39871  dfdisjALTV3  39872  dfdisjALTV4  39873  disjimdmqseq  39881  eldisjs3  39893  eldisjs4  39894  disjsuc  39931  prtlem70  40054  prtlem100  40056  prter2  40078  lsateln0  40192  islshpat  40214  lcvnbtwn3  40225  islfl  40257  ishlat1  40549  ishlat2  40550  cvrat4  40640  islvol5  40776  psubspset  40941  snatpsubN  40947  dalawlem13  41080  psubclsetN  41133  isltrn2N  41317  cdlemftr3  41762  dibelval3  42344  dicval2  42376  dicopelval2  42378  dicelval2N  42379  dihglb2  42539  islpolN  42680  lcfls1c  42733  mapdvalc  42826  mapdval4N  42829  mapdordlem1a  42831  aks4d1p8  43277  fimgmcyc  43738  prjsperref  43774  prjspeclsp  43780  elmzpcl  43877  mzpindd  43897  fphpd  43963  pw2f1ocnv  44184  islmodfg  44211  islssfg2  44213  dflim6  44406  onsucf1olem  44412  omge2  44440  tfsconcatlem  44478  tfsconcat0i  44487  rp-isfinite6  44659  minregex  44675  elmapintrab  44717  elinintrab  44718  relintab  44724  dfrtrcl5  44769  fsovrfovd  45149  ntrk1k3eqk13  45190  gneispace3  45273  k0004lem1  45287  pm13.192  45534  opelopab4  45673  ax6e2nd  45680  en3lplem2VD  45965  ax6e2ndVD  46029  ax6e2ndALT  46051  permaxrep  46135  iuneq1i  46240  ssrabf  46268  limcrecl  46780  dvnprodlem2  47096  fourierdlem103  47358  fourierdlem104  47359  4an21  48479  sprvalpwn0  48704  pairreueq  48731  dfvopnbgr2  49090  isubgredg  49103  xpsnopab  49394  sgrp2sgrp  49464  mpomptx2  49586  lindslinindsimp1  49708  lindslinindsimp2  49714  itsclc0b  50023  mo0sn  50066  coxp  50083  isnat3  50481  fucoisfunc  50626  fucoisfunc2lem2  50628  isthincd2  50711  thinccic  50745  2arwcatlem1  50872  setc1onsubc  50879  alsanmo  51120  ralsanmo  51121  alsralrex  51122  aacllem  51153