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  an33reanOLD  1480  19.26-3an  1873  19.28v  1997  sb3an  2087  19.28  2230  eeeanv  2371  sbel2x  2498  2eu4  2739  r19.26-3  3174  r19.41v  3349  r19.41  3350  rexcomOLD  3358  rexcomf  3360  3reeanv  3370  rabrab  3381  cbvreuw  3445  cbvreu  3449  ceqsex3v  3547  spc2ed  3604  rexab  3688  rexrab  3689  rmo4  3723  rmo3f  3727  reuind  3746  sbc3an  3840  rmo3  3874  rmo3OLD  3875  ssrab  4051  rexun  4168  elin3  4179  inass  4198  rexin  4218  dfun2  4238  indifdir  4262  difin2  4268  inrab2  4278  rabun2  4284  reuun2  4288  undif4  4418  rexdifpr  4600  rexsns  4611  rexdifsn  4729  2ralunsn  4827  iuncom4  4929  iindif1  4999  iunxiun  5021  disjxun  5066  zfrep4  5202  inuni  5248  reusv2lem4  5304  reusv2  5306  otth2  5377  copsexgw  5383  copsexg  5384  copsex4g  5387  opelopabsbALT  5418  rabxp  5602  opeliunxp  5621  xpundir  5623  xpiundi  5624  xpiundir  5625  brinxp2  5631  copsex2gb  5681  dminss  6012  imainss  6013  difxp  6023  cnvresima  6089  coundi  6102  resco  6105  imaco  6106  rnco  6107  coiun  6111  coi1  6117  coass  6120  cnvpo  6140  xpco  6142  wfi  6183  dffun2  6367  fncnv  6429  imadif  6440  mptun  6496  dff1o2  6622  dff1o3  6623  brprcneu  6664  fvun2  6757  eqfnfv3  6806  respreima  6838  f1ompt  6877  f1ossf1o  6892  fsn  6899  fmptsng  6932  fmptsnd  6933  tpres  6965  abrexco  7005  imaiun  7006  f1mpt  7021  dff1o6  7034  oprabidw  7189  oprabid  7190  dfoprab2  7214  oprab4  7242  mpomptx  7267  elpwpwel  7491  elxp4  7629  elxp5  7630  ffoss  7649  f11o  7650  opabex3d  7668  opabex3rd  7669  opabex3  7670  abexssex  7673  elxp7  7726  dfopab2  7752  dfoprab3s  7753  fsplit  7814  frxp  7822  xporderlem  7823  suppssov1  7864  suppssfv  7868  brtpos2  7900  tpostpos  7914  tposmpo  7931  wfrfun  7967  dfrecs3  8011  oarec  8190  oeeu  8231  mapsncnv  8459  dfixp  8465  domen  8524  xpsnen  8603  xpcomco  8609  xpassen  8613  sbthlem9  8637  frfi  8765  marypha2lem2  8902  epfrs  9175  tcsni  9187  cp  9322  dfac5lem1  9551  dfac5lem2  9552  dfac5lem5  9555  kmlem3  9580  dfackm  9594  cfval2  9684  cflim3  9686  cfss  9689  cfslb  9690  zfcndrep  10038  eltsk2g  10175  ltexpi  10326  recmulnq  10388  ltexprlem4  10463  addsrpr  10499  mulsrpr  10500  addcnsr  10559  mulcnsr  10560  ltresr  10564  axrrecex  10587  elnnz  11994  elnn0z  11997  fnn0ind  12084  rexuz2  12302  rexrp  12413  elixx3g  12754  elfz2  12902  elfzuzb  12905  fznn  12978  elfz2nn0  13001  fznn0  13002  4fvwrd4  13030  preduz  13032  elfzo2  13044  fzind2  13158  hashgt23el  13788  hashf1lem1  13816  hashf1lem2  13817  fz1isolem  13822  s4f1o  14282  wwlktovfo  14324  fsum2dlem  15127  modfsummod  15151  sinltx  15544  divalglem10  15755  divalgb  15757  coprmproddvdslem  16008  isprm2  16028  infpn2  16251  prdsle  16737  prdsless  16738  prdsleval  16752  imasleval  16816  xpscf  16840  dfiso2  17044  oppcsect  17050  elhoma  17294  ispos2  17560  lubeldm  17593  glbeldm  17606  tosso  17648  ismhm  17960  issubm  17970  submacs  17993  issubg  18281  issubg3  18299  gaorb  18439  pmtrrn2  18590  efgcpbllema  18882  efgcpbllemb  18883  frgpuplem  18900  subgdmdprd  19158  dprd2d2  19168  dfrhm2  19471  drngprop  19515  drngid2  19520  opprdrng  19528  issubrg  19537  isabv  19592  islss  19708  islbs  19850  lsmspsn  19858  isassa  20090  aspval2  20129  ltbval  20254  opsrle  20258  opsrtoslem1  20266  isobs  20866  islinds  20955  fvmptnn04if  21459  ntreq0  21687  restntr  21792  cnnei  21892  hausnei2  21963  cmpcov2  22000  cmpsub  22010  uncmp  22013  cmpfi  22018  llyi  22084  dissnlocfin  22139  iskgen3  22159  1stckgenlem  22163  ptpjpre1  22181  txcnpi  22218  txtube  22250  hausdiag  22255  txlm  22258  txkgen  22262  cfinfil  22503  csdfil  22504  supfil  22505  fin1aufil  22542  elflim2  22574  hauspwpwf1  22597  txflf  22616  isfcls  22619  alexsubALTlem3  22659  alexsubALT  22661  cnextcn  22677  istmd  22684  istgp  22687  tgphaus  22727  qustgplem  22731  istrg  22774  istdrg  22776  istlm  22795  blres  23043  isms2  23062  metrest  23136  metuel2  23177  restmetu  23182  isngp  23207  isnlm  23286  elii1  23541  isclmp  23703  iscvsp  23734  isncvsngp  23755  iscph  23776  cfilucfil3  23925  isbn  23943  limcrcl  24474  ig1pval3  24770  plydivex  24888  ellogdm  25224  cubic  25429  dmarea  25537  vmasum  25794  lgsquadlem1  25958  lgsquadlem2  25959  istrkg3ld  26249  legov  26373  ltgov  26385  colinearalg  26698  axeuclid  26751  axcontlem2  26753  axcontlem5  26756  nbgrel  27124  nbupgrres  27148  nbusgredgeu0  27152  nb3grprlem2  27165  nb3grpr2  27167  nb3gr2nb  27168  cplgr3v  27219  finsumvtxdg2ssteplem3  27331  wlkonprop  27442  upgrtrls  27485  upgristrl  27486  wksonproplem  27488  usgr2pth0  27548  wwlksnext  27673  wwlksnextsurj  27680  wwlksnfi  27686  wwlksnfiOLD  27687  wspthsnwspthsnon  27697  wpthswwlks2on  27742  rusgrnumwwlkl1  27749  erclwwlkref  27800  isclwwlknx  27816  clwwlknwwlksn  27818  clwwlkel  27827  erclwwlknref  27850  clwlknf1oclwwlkn  27865  clwwlknonel  27876  clwwlknon1  27878  clwwlknon2x  27884  clwwlkvbij  27894  iseupthf1o  27983  2pthfrgrrn  28063  fusgr2wsp2nb  28115  numclwwlk1lem2f1  28138  numclwwlkovh  28154  numclwlk2lem2f1o  28160  frgrregord013  28176  avril1  28244  islno  28532  h2hlm  28759  hcau  28963  hhsssh2  29049  dfch2  29186  elcnop  29636  ellnop  29637  elhmop  29652  elcnfn  29661  ellnfn  29662  dmadjss  29666  adjeu  29668  adjval  29669  hhcno  29683  hhcnf  29684  eleigvec  29736  isst  29992  ishst  29993  cvnbtwn3  30067  cvnbtwn4  30068  chirredi  30173  sumdmdii  30194  or3di  30227  rexunirn  30258  rmoun  30260  dmrab  30262  difrab2  30263  iunin1f  30311  disjunsn  30346  opeldifid  30351  ofpreima  30412  mpomptxf  30427  1stpreima  30444  2ndpreima  30445  f1od2  30459  resf1o  30468  maprnin  30469  nndiffz1  30511  omndmul2  30715  isorng  30874  smatrcl  31063  ordtconnlem1  31169  isrrext  31243  sigaex  31371  sigaval  31372  omssubaddlem  31559  omssubadd  31560  eulerpartleme  31623  eulerpartlemt0  31629  eulerpartlemr  31634  eulerpartlemn  31641  probun  31679  ballotlemelo  31747  ballotlem2  31748  ballotlemfc0  31752  ballotlemfcc  31753  reprdifc  31900  bnj248  31972  bnj250  31973  bnj268  31981  bnj312  31984  bnj945  32047  bnj110  32132  bnj849  32199  bnj882  32200  bnj893  32202  bnj916  32207  bnj983  32225  bnj1040  32246  bnj1175  32278  cusgredgex  32370  cusgr3cyclex  32385  erdszelem1  32440  iscvm  32508  elmpst  32785  mpstrcl  32790  dfso3  32952  coepr  32990  dfpo2  32993  dfdm5  33018  dfrn5  33019  elima4  33021  fv1stcnv  33022  fv2ndcnv  33023  frpoind  33082  frind  33087  soseq  33098  elno3  33164  slenlt  33233  madeval2  33292  brpprod  33348  dfon3  33355  elfix  33366  dffix2  33368  elfuns  33378  brimg  33400  brapply  33401  brsuccf  33404  funpartlem  33405  funpartfun  33406  brrestrict  33412  dfrecs2  33413  dfrdg4  33414  lineunray  33610  ellines  33615  finminlem  33668  fneval  33702  neibastop3  33712  bj-inrab  34247  bj-rest10  34381  bj-restpw  34385  bj-restuni  34390  bj-mpomptALT  34413  icorempo  34634  isbasisrelowllem1  34638  isbasisrelowllem2  34639  relowlpssretop  34647  pibt2  34700  rabiun  34867  iundif1  34868  lindsenlbs  34889  poimirlem4  34898  poimirlem25  34919  poimirlem26  34920  poimirlem29  34923  poimirlem30  34924  ismblfin  34935  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  itg2addnclem2  34946  itg2addnclem3  34947  itg2addnc  34948  ftc1anc  34977  isbnd2  35063  bndss  35066  heibor1lem  35089  heibor1  35090  isrngohom  35245  isidl  35294  sbccom2lem  35404  anan  35501  eqelb  35504  eldmqsres  35545  idinxpssinxp2  35577  moantr  35618  inxpxrn  35645  dfcoss3  35664  cocossss  35683  br1cossinidres  35691  br1cossincnvepres  35692  br1cossxrnidres  35693  br1cossxrncnvepres  35694  refrelcoss2  35706  symrelcoss2  35708  cosscnvssid5  35720  br1cossxrncnvssrres  35750  dfrefrel3  35758  dfcnvrefrel3  35771  cosselcnvrefrels2  35776  cosselcnvrefrels3  35777  cosselcnvrefrels4  35778  cosselcnvrefrels5  35779  dfsymrel3  35788  refsymrel2  35805  refsymrel3  35806  elrefsymrels3  35808  dftrrel3  35816  dfeqvrel2  35827  dfeqvrel3  35828  redundpbi1  35868  refrelredund3  35874  eldmqs1cossres  35895  dffunALTV2  35923  dffunALTV3  35924  dffunALTV4  35925  dffunALTV5  35926  dfdisjALTV  35948  dfdisjALTV2  35949  dfdisjALTV3  35950  dfdisjALTV4  35951  eldisjs3  35959  eldisjs4  35960  prtlem70  35995  prtlem100  35997  prter2  36019  lsateln0  36133  islshpat  36155  lcvnbtwn3  36166  islfl  36198  ishlat1  36490  ishlat2  36491  cvrat4  36581  islvol5  36717  psubspset  36882  snatpsubN  36888  dalawlem13  37021  psubclsetN  37074  isltrn2N  37258  cdlemftr3  37703  dibelval3  38285  dicval2  38317  dicopelval2  38319  dicelval2N  38320  dihglb2  38480  islpolN  38621  lcfls1c  38674  mapdvalc  38767  mapdval4N  38770  mapdordlem1a  38772  prjsperref  39263  prjspeclsp  39269  elmzpcl  39330  mzpindd  39350  fphpd  39420  pw2f1ocnv  39641  islmodfg  39676  islssfg2  39678  isdomn3  39811  rp-isfinite6  39891  elmapintrab  39943  elinintrab  39944  relintab  39950  dfrtrcl5  39996  fsovrfovd  40362  ntrk1k3eqk13  40407  gneispace3  40490  k0004lem1  40504  pm13.192  40749  opelopab4  40892  ax6e2nd  40899  en3lplem2VD  41185  ax6e2ndVD  41249  ax6e2ndALT  41271  ssrabf  41388  limcrecl  41917  dvnprodlem2  42239  fourierdlem103  42501  fourierdlem104  42502  4an21  43476  sprvalpwn0  43652  pairreueq  43679  xpsnopab  44039  ismgmhm  44057  issubmgm  44063  submgmacs  44078  sgrp2sgrp  44142  opeliun2xp  44388  mpomptx2  44390  lindslinindsimp1  44519  lindslinindsimp2  44525  itsclc0b  44766  alsconv  44898  aacllem  44909