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  2084  eeeanv  2350  sbel2x  2474  rexcomf  3271  cbvreu  3387  rabeqi  3408  rabrabi  3414  rabrab  3419  ceqsex3v  3491  spc2ed  3551  rexrab  3650  reurab  3655  rmo3f  3688  reuind  3707  rmo3  3835  ssrab  4018  rexun  4143  elin3  4153  inass  4175  rexin  4197  dfun2  4217  inrab2  4264  rabun2  4271  reuun2  4272  undif4  4414  rexdifpr  4609  rexsns  4621  rexdifsn  4743  2ralunsn  4844  iuncom4  4948  iindif1  5021  iunxiun  5043  disjxun  5087  zfrep4  5229  inuni  5286  reusv2lem4  5337  reusv2  5339  otth2  5421  copsexgw  5428  copsexg  5429  copsex2g  5431  copsex4g  5433  vopelopabsb  5467  rabxp  5662  opeliunxp  5681  opeliun2xp  5682  xpundir  5684  xpiundi  5685  xpiundir  5686  brinxp2  5692  copsex2gb  5745  cnvopab  6083  dminss  6100  imainss  6101  difxp  6111  cnvresima  6177  coundi  6194  resco  6197  imaco  6198  rnco  6199  rncoOLD  6200  coiun  6204  coi1  6210  coass  6213  cnvpo  6234  xpco  6236  dfpo2  6243  frpoind  6289  dffun2  6491  fncnv  6554  imadif  6565  mptun  6627  ffrnb  6665  dff1o2  6768  dff1o3  6769  brprcneu  6812  brprcneuALT  6813  fvun2  6914  eqfnfv3  6966  respreima  6999  f1ompt  7044  f1ossf1o  7061  fsn  7068  fmptsng  7102  fmptsnd  7103  tpres  7135  abrexco  7178  imaiun  7179  f1mpt  7195  dff1o6  7209  imaeqsexvOLD  7297  riotarab  7345  oprabidw  7377  oprabid  7378  dfoprab2  7404  oprab4  7432  mpomptx  7459  elpwpwel  7700  elxp4  7852  elxp5  7853  ffoss  7878  f11o  7879  opabex3d  7897  opabex3rd  7898  opabex3  7899  abexssex  7902  elxp7  7956  dfopab2  7984  dfoprab3s  7985  fsplit  8047  frxp  8056  xporderlem  8057  frpoins3xp3g  8071  soseq  8089  suppssov1  8127  suppssov2  8128  suppssfv  8132  brtpos2  8162  tpostpos  8176  tposmpo  8193  dfrecs3  8292  oarec  8477  oeeu  8518  eldifsucnn  8579  naddasslem1  8609  mapsncnv  8817  dfixp  8823  domen  8884  xpsnen  8974  xpcomco  8980  xpassen  8984  sbthlem9  9008  frfi  9169  marypha2lem2  9320  brttrcl2  9604  epfrs  9621  tcsni  9631  frind  9643  cp  9784  dfac5lem1  10014  dfac5lem2  10015  dfac5lem5  10018  kmlem3  10044  dfackm  10058  cfval2  10151  cflim3  10153  cfss  10156  cfslb  10157  zfcndrep  10505  eltsk2g  10642  ltexpi  10793  recmulnq  10855  ltexprlem4  10930  addsrpr  10966  mulsrpr  10967  addcnsr  11026  mulcnsr  11027  ltresr  11031  axrrecex  11054  elnnz  12478  elnn0z  12481  fnn0ind  12572  rexuz2  12797  rexrp  12913  elixx3g  13258  elfz2  13414  elfzuzb  13418  fznn  13492  elfz2nn0  13518  fznn0  13519  4fvwrd4  13548  preduz  13550  elfzo2  13562  fzind2  13688  hashgt23el  14331  hashf1lem1  14362  hashf1lem2  14363  fz1isolem  14368  s4f1o  14825  wwlktovfo  14865  fsum2dlem  15677  modfsummod  15701  prodeq1i  15823  sinltx  16098  divalglem10  16313  divalgb  16315  coprmproddvdslem  16573  isprm2  16593  infpn2  16825  prdsle  17366  prdsless  17367  prdsleval  17381  imasleval  17445  xpscf  17469  dfiso2  17679  oppcsect  17685  elhoma  17939  ispos2  18221  lubeldm  18257  glbeldm  18270  tosso  18323  ismgmhm  18604  issubmgm  18610  submgmacs  18625  ismhm  18693  issubm  18711  submacs  18735  issubg  19039  issubg3  19057  gaorb  19219  pmtrrn2  19372  efgcpbllema  19666  efgcpbllemb  19667  frgpuplem  19684  imasabl  19788  subgdmdprd  19948  dprd2d2  19958  omndmul2  20045  dfrhm2  20392  opprnzrb  20436  issubrg  20486  isdomn3  20630  drngprop  20659  drngid2  20667  opprdrng  20679  isabv  20726  isorng  20776  islss  20867  islbs  21010  lsmspsn  21018  isobs  21657  islinds  21746  isassa  21793  aspval2  21835  ltbval  21978  opsrle  21982  opsrtoslem1  21990  fvmptnn04if  22764  ntreq0  22992  restntr  23097  cnnei  23197  hausnei2  23268  cmpcov2  23305  cmpsub  23315  uncmp  23318  cmpfi  23323  llyi  23389  dissnlocfin  23444  iskgen3  23464  1stckgenlem  23468  ptpjpre1  23486  txcnpi  23523  txtube  23555  hausdiag  23560  txlm  23563  txkgen  23567  cfinfil  23808  csdfil  23809  supfil  23810  fin1aufil  23847  elflim2  23879  hauspwpwf1  23902  txflf  23921  isfcls  23924  alexsubALTlem3  23964  alexsubALT  23966  cnextcn  23982  istmd  23989  istgp  23992  tgphaus  24032  qustgplem  24036  istrg  24079  istdrg  24081  istlm  24100  blres  24346  isms2  24365  metrest  24439  metuel2  24480  restmetu  24485  isngp  24511  isnlm  24590  elii1  24858  isclmp  25024  iscvsp  25055  isncvsngp  25076  iscph  25097  cfilucfil3  25247  isbn  25265  limcrcl  25802  ig1pval3  26110  plydivex  26232  ellogdm  26575  cubic  26786  dmarea  26894  vmasum  27154  lgsquadlem1  27318  lgsquadlem2  27319  elno3  27594  slenlt  27691  madeval2  27794  elnnzs  28325  istrkg3ld  28439  legov  28563  ltgov  28575  colinearalg  28888  axeuclid  28941  axcontlem2  28943  axcontlem5  28946  nbgrel  29318  nbupgrres  29342  nbusgredgeu0  29346  nb3grprlem2  29359  nb3grpr2  29361  nb3gr2nb  29362  cplgr3v  29413  finsumvtxdg2ssteplem3  29526  wlkonprop  29635  upgrtrls  29678  upgristrl  29679  wksonproplem  29681  usgr2pth0  29743  wwlksnext  29871  wwlksnextsurj  29878  wwlksnfi  29884  wspthsnwspthsnon  29894  wpthswwlks2on  29942  rusgrnumwwlkl1  29949  erclwwlkref  30000  isclwwlknx  30016  clwwlknwwlksn  30018  clwwlkel  30026  erclwwlknref  30049  clwlknf1oclwwlkn  30064  clwwlknonel  30075  clwwlknon1  30077  clwwlknon2x  30083  clwwlkvbij  30093  iseupthf1o  30182  2pthfrgrrn  30262  fusgr2wsp2nb  30314  numclwwlk1lem2f1  30337  numclwwlkovh  30353  numclwlk2lem2f1o  30359  frgrregord013  30375  avril1  30443  islno  30733  h2hlm  30960  hcau  31164  hhsssh2  31250  dfch2  31387  elcnop  31837  ellnop  31838  elhmop  31853  elcnfn  31862  ellnfn  31863  dmadjss  31867  adjeu  31869  adjval  31870  hhcno  31884  hhcnf  31885  eleigvec  31937  isst  32193  ishst  32194  cvnbtwn3  32268  cvnbtwn4  32269  chirredi  32374  sumdmdii  32395  an52ds  32430  an62ds  32431  an72ds  32432  an82ds  32433  or3di  32438  rexunirn  32471  rmoun  32473  dmrab  32476  difrab2  32477  iunin1f  32537  disjunsn  32574  opeldifid  32579  ofpreima  32647  mpomptxf  32659  fdifsupp  32666  1stpreima  32688  2ndpreima  32689  f1od2  32702  resf1o  32713  maprnin  32714  nndiffz1  32769  ismnt  32964  mgcval  32968  erler  33232  opprnsg  33449  1arithidom  33502  1arithufdlem4  33512  extdgfialglem1  33705  smatrcl  33809  ordtconnlem1  33937  isrrext  34013  sigaex  34123  sigaval  34124  omssubaddlem  34312  omssubadd  34313  eulerpartleme  34376  eulerpartlemt0  34382  eulerpartlemr  34387  eulerpartlemn  34394  probun  34432  ballotlemelo  34501  ballotlem2  34502  ballotlemfc0  34506  ballotlemfcc  34507  reprdifc  34640  bnj248  34712  bnj250  34713  bnj268  34721  bnj312  34724  bnj945  34785  bnj110  34870  bnj849  34937  bnj882  34938  bnj893  34940  bnj916  34945  bnj983  34963  bnj1040  34984  bnj1175  35016  cusgredgex  35166  cusgr3cyclex  35180  erdszelem1  35235  iscvm  35303  elmpst  35580  mpstrcl  35585  dfso3  35764  xpab  35770  coepr  35797  dfdm5  35817  dfrn5  35818  elima4  35820  fv1stcnv  35821  fv2ndcnv  35822  brpprod  35927  dfon3  35934  elfix  35945  dffix2  35947  elfuns  35957  brimg  35979  brapply  35980  brsuccf  35983  funpartlem  35984  funpartfun  35985  brrestrict  35991  dfrecs2  35992  dfrdg4  35993  lineunray  36189  ellines  36194  rmoeqi  36229  reueqi  36231  itgeq12i  36248  finminlem  36360  fneval  36394  neibastop3  36404  eliminable-abelv  36911  bj-inrab  36969  bj-rest10  37130  bj-restpw  37134  bj-restuni  37139  bj-mpomptALT  37161  bj-imdirco  37232  icorempo  37393  isbasisrelowllem1  37397  isbasisrelowllem2  37398  relowlpssretop  37406  pibt2  37459  wl-ifp-ncond2  37507  wl-df3-3mintru2  37528  wl-2mintru1  37532  rabiun  37641  iundif1  37642  lindsenlbs  37663  poimirlem4  37672  poimirlem25  37693  poimirlem26  37694  poimirlem29  37697  poimirlem30  37698  ismblfin  37709  ovoliunnfl  37710  voliunnfl  37712  volsupnfl  37713  itg2addnclem2  37720  itg2addnclem3  37721  itg2addnc  37722  ftc1anc  37749  isbnd2  37831  bndss  37834  heibor1lem  37857  heibor1  37858  isrngohom  38013  isidl  38062  sbccom2lem  38172  anan  38271  eqbrb  38275  eqelb  38277  br1cnvinxp  38299  eldmqsres  38329  idinxpssinxp2  38360  moantr  38400  inxpxrn  38435  dfcoss3  38459  cocossss  38481  ressn2  38487  br1cossinidres  38494  br1cossincnvepres  38495  br1cossxrnidres  38496  br1cossxrncnvepres  38497  refrelcoss2  38509  symrelcoss2  38511  cosscnvssid5  38523  br1cossxrncnvssrres  38553  dfrefrel3  38561  dfcnvrefrel3  38576  cosselcnvrefrels2  38583  cosselcnvrefrels3  38584  cosselcnvrefrels4  38585  cosselcnvrefrels5  38586  dfsymrel3  38595  refsymrel2  38612  refsymrel3  38613  elrefsymrels3  38615  dftrrel3  38623  dfeqvrel2  38635  dfeqvrel3  38636  redundpbi1  38676  refrelredund3  38682  eldmqs1cossres  38705  dffunALTV2  38734  dffunALTV3  38735  dffunALTV4  38736  dffunALTV5  38737  dfdisjALTV  38759  dfdisjALTV2  38760  dfdisjALTV3  38761  dfdisjALTV4  38762  eldisjs3  38770  eldisjs4  38771  disjsuc  38805  prtlem70  38904  prtlem100  38906  prter2  38928  lsateln0  39042  islshpat  39064  lcvnbtwn3  39075  islfl  39107  ishlat1  39399  ishlat2  39400  cvrat4  39490  islvol5  39626  psubspset  39791  snatpsubN  39797  dalawlem13  39930  psubclsetN  39983  isltrn2N  40167  cdlemftr3  40612  dibelval3  41194  dicval2  41226  dicopelval2  41228  dicelval2N  41229  dihglb2  41389  islpolN  41530  lcfls1c  41583  mapdvalc  41676  mapdval4N  41679  mapdordlem1a  41681  aks4d1p8  42128  fimgmcyc  42575  prjsperref  42647  prjspeclsp  42653  elmzpcl  42767  mzpindd  42787  fphpd  42857  pw2f1ocnv  43078  islmodfg  43110  islssfg2  43112  dflim6  43305  onsucf1olem  43311  omge2  43339  tfsconcatlem  43377  tfsconcat0i  43386  rp-isfinite6  43559  minregex  43575  elmapintrab  43617  elinintrab  43618  relintab  43624  dfrtrcl5  43670  fsovrfovd  44050  ntrk1k3eqk13  44091  gneispace3  44174  k0004lem1  44188  pm13.192  44451  opelopab4  44592  ax6e2nd  44599  en3lplem2VD  44884  ax6e2ndVD  44948  ax6e2ndALT  44970  permaxrep  45047  iuneq1i  45130  ssrabf  45159  limcrecl  45677  dvnprodlem2  45993  fourierdlem103  46255  fourierdlem104  46256  4an21  47309  sprvalpwn0  47522  pairreueq  47549  dfvopnbgr2  47892  isubgredg  47905  xpsnopab  48196  sgrp2sgrp  48267  mpomptx2  48374  lindslinindsimp1  48497  lindslinindsimp2  48503  itsclc0b  48812  mo0sn  48855  coxp  48872  isthincd2  49477  thinccic  49511  2arwcatlem1  49635  setc1onsubc  49642  alsconv  49830  aacllem  49841