Theorem anbi1i 625

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  anbi2ci  626  anbi12i  628  bianassc  641  anandi  674  pm5.53  1001  dfifp4  1061  dfifp5  1062  3an4anass  1101  3ioran  1102  an6  1441  an3andi  1478  an33rean  1479  19.26-3an  1869  19.28v  1993  sb3an  2083  19.28  2226  eeeanv  2367  sbel2x  2494  2eu4  2737  r19.26-3  3172  r19.41v  3347  r19.41  3348  rexcomOLD  3356  rexcomf  3358  3reeanv  3368  rabrab  3379  cbvreuw  3443  cbvreu  3447  ceqsex3v  3545  spc2ed  3601  rexab  3685  rexrab  3686  rmo4  3720  rmo3f  3724  reuind  3743  sbc3an  3837  rmo3  3871  rmo3OLD  3872  ssrab  4048  rexun  4165  elin3  4176  inass  4195  rexin  4215  dfun2  4235  indifdir  4259  difin2  4265  inrab2  4275  rabun2  4281  reuun2  4285  undif4  4415  rexdifpr  4597  rexsns  4608  rexdifsn  4726  2ralunsn  4824  iuncom4  4926  iindif1  4996  iunxiun  5018  disjxun  5063  zfrep4  5199  inuni  5245  reusv2lem4  5301  reusv2  5303  otth2  5374  copsexgw  5380  copsexg  5381  copsex4g  5384  opelopabsbALT  5415  rabxp  5599  opeliunxp  5618  xpundir  5620  xpiundi  5621  xpiundir  5622  brinxp2  5628  copsex2gb  5678  dminss  6009  imainss  6010  difxp  6020  cnvresima  6086  coundi  6099  resco  6102  imaco  6103  rnco  6104  coiun  6108  coi1  6114  coass  6117  cnvpo  6137  xpco  6139  wfi  6180  dffun2  6364  fncnv  6426  imadif  6437  mptun  6493  dff1o2  6619  dff1o3  6620  brprcneu  6661  fvun2  6754  eqfnfv3  6803  respreima  6835  f1ompt  6874  f1ossf1o  6889  fsn  6896  fmptsng  6929  fmptsnd  6930  tpres  6962  abrexco  7002  imaiun  7003  f1mpt  7018  dff1o6  7031  oprabidw  7186  oprabid  7187  dfoprab2  7211  oprab4  7239  mpomptx  7264  elpwpwel  7488  elxp4  7626  elxp5  7627  ffoss  7646  f11o  7647  opabex3d  7665  opabex3rd  7666  opabex3  7667  abexssex  7670  elxp7  7723  dfopab2  7749  dfoprab3s  7750  fsplit  7811  frxp  7819  xporderlem  7820  suppssov1  7861  suppssfv  7865  brtpos2  7897  tpostpos  7911  tposmpo  7928  wfrfun  7964  dfrecs3  8008  oarec  8187  oeeu  8228  mapsncnv  8456  dfixp  8462  domen  8521  xpsnen  8600  xpcomco  8606  xpassen  8610  sbthlem9  8634  frfi  8762  marypha2lem2  8899  epfrs  9172  tcsni  9184  cp  9319  dfac5lem1  9548  dfac5lem2  9549  dfac5lem5  9552  kmlem3  9577  dfackm  9591  cfval2  9681  cflim3  9683  cfss  9686  cfslb  9687  zfcndrep  10035  eltsk2g  10172  ltexpi  10323  recmulnq  10385  ltexprlem4  10460  addsrpr  10496  mulsrpr  10497  addcnsr  10556  mulcnsr  10557  ltresr  10561  axrrecex  10584  elnnz  11990  elnn0z  11993  fnn0ind  12080  rexuz2  12298  rexrp  12409  elixx3g  12750  elfz2  12898  elfzuzb  12901  fznn  12974  elfz2nn0  12997  fznn0  12998  4fvwrd4  13026  preduz  13028  elfzo2  13040  fzind2  13154  hashgt23el  13784  hashf1lem1  13812  hashf1lem2  13813  fz1isolem  13818  s4f1o  14279  wwlktovfo  14321  fsum2dlem  15124  modfsummod  15148  sinltx  15541  divalglem10  15752  divalgb  15754  coprmproddvdslem  16005  isprm2  16025  infpn2  16248  prdsle  16734  prdsless  16735  prdsleval  16749  imasleval  16813  xpscf  16837  dfiso2  17041  oppcsect  17047  elhoma  17291  ispos2  17557  lubeldm  17590  glbeldm  17603  tosso  17645  ismhm  17957  issubm  17967  submacs  17990  issubg  18278  issubg3  18296  gaorb  18436  pmtrrn2  18587  efgcpbllema  18879  efgcpbllemb  18880  frgpuplem  18897  subgdmdprd  19155  dprd2d2  19165  dfrhm2  19468  drngprop  19512  drngid2  19517  opprdrng  19525  issubrg  19534  isabv  19589  islss  19705  islbs  19847  lsmspsn  19855  isassa  20087  aspval2  20126  ltbval  20251  opsrle  20255  opsrtoslem1  20263  isobs  20863  islinds  20952  fvmptnn04if  21456  ntreq0  21684  restntr  21789  cnnei  21889  hausnei2  21960  cmpcov2  21997  cmpsub  22007  uncmp  22010  cmpfi  22015  llyi  22081  dissnlocfin  22136  iskgen3  22156  1stckgenlem  22160  ptpjpre1  22178  txcnpi  22215  txtube  22247  hausdiag  22252  txlm  22255  txkgen  22259  cfinfil  22500  csdfil  22501  supfil  22502  fin1aufil  22539  elflim2  22571  hauspwpwf1  22594  txflf  22613  isfcls  22616  alexsubALTlem3  22656  alexsubALT  22658  cnextcn  22674  istmd  22681  istgp  22684  tgphaus  22724  qustgplem  22728  istrg  22771  istdrg  22773  istlm  22792  blres  23040  isms2  23059  metrest  23133  metuel2  23174  restmetu  23179  isngp  23204  isnlm  23283  elii1  23538  isclmp  23700  iscvsp  23731  isncvsngp  23752  iscph  23773  cfilucfil3  23922  isbn  23940  limcrcl  24471  ig1pval3  24767  plydivex  24885  ellogdm  25221  cubic  25426  dmarea  25534  vmasum  25791  lgsquadlem1  25955  lgsquadlem2  25956  istrkg3ld  26246  legov  26370  ltgov  26382  colinearalg  26695  axeuclid  26748  axcontlem2  26750  axcontlem5  26753  nbgrel  27121  nbupgrres  27145  nbusgredgeu0  27149  nb3grprlem2  27162  nb3grpr2  27164  nb3gr2nb  27165  cplgr3v  27216  finsumvtxdg2ssteplem3  27328  wlkonprop  27439  upgrtrls  27482  upgristrl  27483  wksonproplem  27485  usgr2pth0  27545  wwlksnext  27670  wwlksnextsurj  27677  wwlksnfi  27683  wwlksnfiOLD  27684  wspthsnwspthsnon  27694  wpthswwlks2on  27739  rusgrnumwwlkl1  27746  erclwwlkref  27797  isclwwlknx  27813  clwwlknwwlksn  27815  clwwlkel  27824  erclwwlknref  27847  clwlknf1oclwwlkn  27862  clwwlknonel  27873  clwwlknon1  27875  clwwlknon2x  27881  clwwlkvbij  27891  iseupthf1o  27980  2pthfrgrrn  28060  fusgr2wsp2nb  28112  numclwwlk1lem2f1  28135  numclwwlkovh  28151  numclwlk2lem2f1o  28157  frgrregord013  28173  avril1  28241  islno  28529  h2hlm  28756  hcau  28960  hhsssh2  29046  dfch2  29183  elcnop  29633  ellnop  29634  elhmop  29649  elcnfn  29658  ellnfn  29659  dmadjss  29663  adjeu  29665  adjval  29666  hhcno  29680  hhcnf  29681  eleigvec  29733  isst  29989  ishst  29990  cvnbtwn3  30064  cvnbtwn4  30065  chirredi  30170  sumdmdii  30191  or3di  30224  rexunirn  30255  rmoun  30257  dmrab  30259  difrab2  30260  iunin1f  30308  disjunsn  30343  opeldifid  30348  ofpreima  30409  mpomptxf  30424  1stpreima  30441  2ndpreima  30442  f1od2  30456  resf1o  30465  maprnin  30466  nndiffz1  30508  omndmul2  30713  isorng  30872  smatrcl  31061  ordtconnlem1  31167  isrrext  31241  sigaex  31369  sigaval  31370  omssubaddlem  31557  omssubadd  31558  eulerpartleme  31621  eulerpartlemt0  31627  eulerpartlemr  31632  eulerpartlemn  31639  probun  31677  ballotlemelo  31745  ballotlem2  31746  ballotlemfc0  31750  ballotlemfcc  31751  reprdifc  31898  bnj248  31970  bnj250  31971  bnj268  31979  bnj312  31982  bnj945  32045  bnj110  32130  bnj849  32197  bnj882  32198  bnj893  32200  bnj916  32205  bnj983  32223  bnj1040  32244  bnj1175  32276  cusgredgex  32368  cusgr3cyclex  32383  erdszelem1  32438  iscvm  32506  elmpst  32783  mpstrcl  32788  dfso3  32950  coepr  32988  dfpo2  32991  dfdm5  33016  dfrn5  33017  elima4  33019  fv1stcnv  33020  fv2ndcnv  33021  frpoind  33080  frind  33085  soseq  33096  elno3  33162  slenlt  33231  madeval2  33290  brpprod  33346  dfon3  33353  elfix  33364  dffix2  33366  elfuns  33376  brimg  33398  brapply  33399  brsuccf  33402  funpartlem  33403  funpartfun  33404  brrestrict  33410  dfrecs2  33411  dfrdg4  33412  lineunray  33608  ellines  33613  finminlem  33666  fneval  33700  neibastop3  33710  bj-inrab  34245  bj-rest10  34378  bj-restpw  34382  bj-restuni  34387  bj-mpomptALT  34410  icorempo  34631  isbasisrelowllem1  34635  isbasisrelowllem2  34636  relowlpssretop  34644  pibt2  34697  rabiun  34864  iundif1  34865  lindsenlbs  34886  poimirlem4  34895  poimirlem25  34916  poimirlem26  34917  poimirlem29  34920  poimirlem30  34921  ismblfin  34932  ovoliunnfl  34933  voliunnfl  34935  volsupnfl  34936  itg2addnclem2  34943  itg2addnclem3  34944  itg2addnc  34945  ftc1anc  34974  isbnd2  35060  bndss  35063  heibor1lem  35086  heibor1  35087  isrngohom  35242  isidl  35291  sbccom2lem  35401  anan  35498  eqelb  35501  eldmqsres  35542  idinxpssinxp2  35574  moantr  35615  inxpxrn  35642  dfcoss3  35661  cocossss  35680  br1cossinidres  35688  br1cossincnvepres  35689  br1cossxrnidres  35690  br1cossxrncnvepres  35691  refrelcoss2  35703  symrelcoss2  35705  cosscnvssid5  35717  br1cossxrncnvssrres  35747  dfrefrel3  35755  dfcnvrefrel3  35768  cosselcnvrefrels2  35773  cosselcnvrefrels3  35774  cosselcnvrefrels4  35775  cosselcnvrefrels5  35776  dfsymrel3  35785  refsymrel2  35802  refsymrel3  35803  elrefsymrels3  35805  dftrrel3  35813  dfeqvrel2  35824  dfeqvrel3  35825  redundpbi1  35865  refrelredund3  35871  eldmqs1cossres  35892  dffunALTV2  35920  dffunALTV3  35921  dffunALTV4  35922  dffunALTV5  35923  dfdisjALTV  35945  dfdisjALTV2  35946  dfdisjALTV3  35947  dfdisjALTV4  35948  eldisjs3  35956  eldisjs4  35957  prtlem70  35992  prtlem100  35994  prter2  36016  lsateln0  36130  islshpat  36152  lcvnbtwn3  36163  islfl  36195  ishlat1  36487  ishlat2  36488  cvrat4  36578  islvol5  36714  psubspset  36879  snatpsubN  36885  dalawlem13  37018  psubclsetN  37071  isltrn2N  37255  cdlemftr3  37700  dibelval3  38282  dicval2  38314  dicopelval2  38316  dicelval2N  38317  dihglb2  38477  islpolN  38618  lcfls1c  38671  mapdvalc  38764  mapdval4N  38767  mapdordlem1a  38769  prjsperref  39254  prjspeclsp  39260  elmzpcl  39321  mzpindd  39341  fphpd  39411  pw2f1ocnv  39632  islmodfg  39667  islssfg2  39669  isdomn3  39802  rp-isfinite6  39882  elmapintrab  39934  elinintrab  39935  relintab  39941  dfrtrcl5  39987  fsovrfovd  40353  ntrk1k3eqk13  40398  gneispace3  40481  k0004lem1  40495  pm13.192  40740  opelopab4  40883  ax6e2nd  40890  en3lplem2VD  41176  ax6e2ndVD  41240  ax6e2ndALT  41262  ssrabf  41379  limcrecl  41908  dvnprodlem2  42230  fourierdlem103  42493  fourierdlem104  42494  4an21  43468  sprvalpwn0  43644  pairreueq  43671  xpsnopab  44031  ismgmhm  44049  issubmgm  44055  submgmacs  44070  sgrp2sgrp  44134  opeliun2xp  44380  mpomptx2  44382  lindslinindsimp1  44511  lindslinindsimp2  44517  itsclc0b  44758  alsconv  44890  aacllem  44901