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  1520  19.26-3an  1905  sb3an  2118  eeeanv  2384  sbel2x  2508  rexcomf  3306  cbvreu  3410  rabeqi  3431  rabrabi  3437  rabrab  3442  ceqsex3v  3509  spc2ed  3562  rexrab  3661  reurab  3666  rmo3f  3699  reuind  3718  rmo3  3843  ssrab  4026  rexun  4149  elin3  4159  inass  4180  rexin  4203  dfun2  4223  inrab2  4270  rabun2  4277  reuun2  4278  undif4  4427  rexdifpr  4627  rexsns  4639  rexdifsn  4764  2ralunsn  4862  iuncom4  4967  iindif1  5043  iunxiun  5065  disjxun  5109  zfrep4  5256  inuni  5322  reusv2lem4  5374  reusv2  5376  otth2  5467  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  copsex2g  5478  copsex4g  5480  vopelopabsb  5515  rabxp  5711  opeliunxp  5730  opeliun2xp  5731  xpundir  5733  xpiundi  5734  xpiundir  5735  brinxp2  5741  copsex2gb  5795  cnvopab  6139  dminss  6152  imainss  6153  difxp  6163  cnvresima  6233  coundi  6250  resco  6253  imaco  6254  rnco  6255  rncoOLD  6256  coiun  6260  coi1  6266  coass  6269  cnvpo  6292  xpco  6294  dfpo2  6301  frpoind  6347  dffun2  6550  fncnv  6613  imadif  6624  mptun  6685  ffrnb  6724  dff1o2  6830  dff1o3  6831  brprcneu  6875  brprcneuALT  6876  fvun2  6977  eqfnfv3  7031  respreima  7065  f1ompt  7110  f1ossf1o  7128  fsn  7135  fmptsng  7172  fmptsnd  7173  tpres  7206  abrexco  7247  imaiun  7248  f1mpt  7264  dff1o6  7282  riotarab  7418  oprabidw  7450  oprabid  7451  dfoprab2  7477  oprab4  7505  mpomptx  7532  elpwpwel  7772  elxp4  7925  elxp5  7926  ffoss  7949  f11o  7950  opabex3d  7968  opabex3rd  7969  opabex3  7970  abexssex  7973  elxp7  8027  dfopab2  8055  dfoprab3s  8056  fsplit  8118  frxp  8128  xporderlem  8129  frpoins3xp3g  8143  soseq  8161  suppssov1  8199  suppssov2  8200  suppssfv  8204  brtpos2  8234  tpostpos  8248  tposmpo  8265  dfrecs3  8365  oarec  8553  oeeu  8595  eldifsucnn  8656  naddasslem1  8687  mapsncnv  8897  dfixp  8903  domen  8964  xpsnen  9056  xpcomco  9062  xpassen  9066  sbthlem9  9090  frfi  9252  marypha2lem2  9403  brttrcl2  9690  epfrs  9707  tcsni  9717  frind  9729  cp  9890  dfac5lem1  10123  dfac5lem2  10124  dfac5lem5  10127  kmlem3  10152  dfackm  10166  cfval2  10259  cflim3  10261  cfss  10264  cfslb  10265  zfcndrep  10616  eltsk2g  10753  ltexpi  10904  recmulnq  10966  ltexprlem4  11041  addsrpr  11077  mulsrpr  11078  addcnsr  11137  mulcnsr  11138  ltresr  11142  axrrecex  11165  elnnz  12618  elnn0z  12621  fnn0ind  12713  rexuz2  12941  rexrp  13057  elixx3g  13403  elfz2  13560  elfzuzb  13564  fznn  13639  elfz2nn0  13665  fznn0  13666  4fvwrd4  13695  preduz  13697  elfzo2  13709  fzind2  13836  hashgt23el  14481  hashf1lem1  14512  hashf1lem2  14513  fz1isolem  14518  s4f1o  14981  wwlktovfo  15021  fsum2dlem  15846  modfsummod  15871  prodeq1i  15995  sinltx  16269  divalglem10  16484  divalgb  16486  coprmproddvdslem  16744  isprm2  16764  infpn2  16997  prdsle  17539  prdsless  17540  prdsleval  17554  imasleval  17619  xpscf  17643  dfiso2  17853  oppcsect  17859  elhoma  18113  ispos2  18395  lubeldm  18431  glbeldm  18444  tosso  18497  ismgmhm  18788  issubmgm  18794  submgmacs  18809  ismhm  18882  issubm  18900  submacs  18925  issubg  19238  issubg3  19257  gaorb  19423  pmtrrn2  19576  efgcpbllema  19870  efgcpbllemb  19871  frgpuplem  19888  imasabl  19992  subgdmdprd  20152  dprd2d2  20162  omndmul2  20249  dfrhm2  20604  isrhm0  20606  opprnzrb  20671  issubrg  20722  isdomn3  20865  drngprop  20896  drngid2  20908  opprdrng  20919  isabv  20966  isorng  21016  islss  21107  islbs  21249  lsmspsn  21257  isobs  21922  islinds  22011  isassa  22058  aspval2  22100  ltbval  22246  opsrle  22250  opsrtoslem1  22258  fvmptnn04if  23058  ntreq0  23286  restntr  23391  cnnei  23491  hausnei2  23562  cmpcov2  23599  cmpsub  23609  uncmp  23612  cmpfi  23617  llyi  23684  dissnlocfin  23739  iskgen3  23759  1stckgenlem  23763  ptpjpre1  23781  txcnpi  23818  txtube  23850  hausdiag  23855  txlm  23858  txkgen  23862  cfinfil  24103  csdfil  24104  supfil  24105  fin1aufil  24142  elflim2  24174  hauspwpwf1  24197  txflf  24216  isfcls  24219  alexsubALTlem3  24259  alexsubALT  24261  cnextcn  24277  istmd  24284  istgp  24287  tgphaus  24327  qustgplem  24331  istrg  24374  istdrg  24376  istlm  24395  blres  24641  isms2  24660  metrest  24734  metuel2  24775  restmetu  24780  isngp  24806  isnlm  24885  elii1  25147  isclmp  25309  iscvsp  25340  isncvsngp  25361  iscph  25382  cfilucfil3  25532  isbn  25550  limcrcl  26086  ig1pval3  26388  plydivex  26511  ellogdm  26857  cubic  27067  dmarea  27175  vmasum  27433  lgsquadlem1  27597  lgsquadlem2  27598  elno3  27872  lenlts  27969  madeval2  28079  elnnzs  28647  istrkg3ld  28783  legov  28907  ltgov  28919  colinearalg  29317  axeuclid  29370  axcontlem2  29372  axcontlem5  29375  nbgrel  29750  nbupgrres  29774  nbusgredgeu0  29778  nb3grprlem2  29791  nb3grpr2  29793  nb3gr2nb  29794  cplgr3v  29845  finsumvtxdg2ssteplem3  29957  wlkonprop  30066  upgrtrls  30113  upgristrl  30114  wksonproplem  30116  usgr2pth0  30180  wwlksnext  30311  wwlksnextsurj  30318  wwlksnfi  30324  wspthsnwspthsnon  30334  wpthswwlks2on  30382  rusgrnumwwlkl1  30389  erclwwlkref  30440  isclwwlknx  30456  clwwlknwwlksn  30458  clwwlkel  30466  erclwwlknref  30489  clwlknf1oclwwlkn  30504  clwwlknonel  30515  clwwlknon1  30517  clwwlknon2x  30523  clwwlkvbij  30533  iseupthf1o  30626  2pthfrgrrn  30706  fusgr2wsp2nb  30758  numclwwlk1lem2f1  30781  numclwwlkovh  30797  numclwlk2lem2f1o  30803  frgrregord013  30819  avril1  30887  islno  31178  h2hlm  31405  hcau  31609  hhsssh2  31695  dfch2  31832  elcnop  32282  ellnop  32283  elhmop  32298  elcnfn  32307  ellnfn  32308  dmadjss  32312  adjeu  32314  adjval  32315  hhcno  32329  hhcnf  32330  eleigvec  32382  isst  32638  ishst  32639  cvnbtwn3  32713  cvnbtwn4  32714  chirredi  32819  sumdmdii  32840  an52ds  32875  an62ds  32876  an72ds  32877  an82ds  32878  or3di  32880  rexunirn  32911  rmoun  32913  dmrab  32916  difrab2  32917  iunin1f  32975  disjunsn  33012  opeldifid  33017  ofpreima  33083  mpomptxf  33096  fdifsupp  33103  1stpreima  33125  2ndpreima  33126  f1od2  33136  resf1o  33147  maprnin  33148  nndiffz1  33203  ismnt  33369  mgcval  33373  erler  33651  opprnsg  33832  1arithidom  33893  1arithufdlem4  33903  extdgfialglem1  34148  smatrcl  34252  ordtconnlem1  34380  isrrext  34456  sigaex  34566  sigaval  34567  omssubaddlem  34756  omssubadd  34757  eulerpartleme  34820  eulerpartlemt0  34826  eulerpartlemr  34831  eulerpartlemn  34838  probun  34876  ballotlemelo  34945  ballotlem2  34946  ballotlemfc0  34950  ballotlemfcc  34951  reprdifc  35081  bnj248  35156  bnj250  35157  bnj268  35165  bnj312  35168  bnj945  35229  bnj110  35313  bnj849  35380  bnj882  35381  bnj893  35383  bnj916  35388  bnj983  35406  bnj1040  35427  bnj1175  35459  cusgredgex  35666  cusgr3cyclex  35671  erdszelem1  35722  iscvm  35790  elmpst  36067  mpstrcl  36072  dfso3  36251  xpab  36257  coepr  36284  dfdm5  36304  dfrn5  36305  elima4  36307  fv1stcnv  36308  fv2ndcnv  36309  brpprod  36414  dfon3  36421  elfix  36432  dffix2  36434  elfuns  36444  brimg  36466  brapply  36467  lemsuccf  36470  funpartlem  36473  funpartfun  36474  brrestrict  36480  dfrecs2  36481  dfrdg4  36482  lineunray  36678  ellines  36683  rmoeqi  36758  reueqi  36760  itgeq12i  36777  finminlem  36888  fneval  36922  neibastop3  36932  eliminable-abelv  37563  bj-inrab  37622  bj-axseprep  37770  bj-rest10  37789  bj-restpw  37793  bj-restuni  37798  bj-mpomptALT  37820  copsex2gd  37841  bj-imdirco  37893  icorempo  38056  isbasisrelowllem1  38060  isbasisrelowllem2  38061  relowlpssretop  38069  pibt2  38122  wl-ifp-ncond2  38170  wl-df3-3mintru2  38191  wl-2mintru1  38195  rabiun  38303  iundif1  38304  lindsenlbs  38325  poimirlem4  38334  poimirlem25  38355  poimirlem26  38356  poimirlem29  38359  poimirlem30  38360  ismblfin  38371  ovoliunnfl  38372  voliunnfl  38374  volsupnfl  38375  itg2addnclem2  38382  itg2addnclem3  38383  itg2addnc  38384  ftc1anc  38411  isbnd2  38494  bndss  38497  heibor1lem  38520  heibor1  38521  isrngohom  38676  isidl  38725  sbccom2lem  38833  anan  38944  eqbrb  38948  eqelb  38950  br1cnvinxp  38968  eldmqsres  39002  idinxpssinxp2  39033  moantr  39081  inxpxrn  39127  blockadjliftmap  39167  dfcoss3  39213  cocossss  39235  ressn2  39241  br1cossinidres  39248  br1cossincnvepres  39249  br1cossxrnidres  39250  br1cossxrncnvepres  39251  refrelcoss2  39263  symrelcoss2  39265  cosscnvssid5  39277  br1cossxrncnvssrres  39297  dfrefrel3  39305  dfcnvrefrel3  39320  cosselcnvrefrels2  39327  cosselcnvrefrels3  39328  cosselcnvrefrels4  39329  cosselcnvrefrels5  39330  dfsymrel3  39343  refsymrel2  39360  refsymrel3  39361  elrefsymrels3  39363  dftrrel3  39371  dfeqvrel2  39383  dfeqvrel3  39384  redundpbi1  39424  refrelredund3  39430  eldmqs1cossres  39453  dffunALTV2  39482  dffunALTV3  39483  dffunALTV4  39484  dffunALTV5  39485  dfdisjALTV  39507  dfdisjALTV2  39508  dfdisjALTV3  39509  dfdisjALTV4  39510  disjimdmqseq  39518  eldisjs3  39530  eldisjs4  39531  disjsuc  39568  prtlem70  39691  prtlem100  39693  prter2  39715  lsateln0  39829  islshpat  39851  lcvnbtwn3  39862  islfl  39894  ishlat1  40186  ishlat2  40187  cvrat4  40277  islvol5  40413  psubspset  40578  snatpsubN  40584  dalawlem13  40717  psubclsetN  40770  isltrn2N  40954  cdlemftr3  41399  dibelval3  41981  dicval2  42013  dicopelval2  42015  dicelval2N  42016  dihglb2  42176  islpolN  42317  lcfls1c  42370  mapdvalc  42463  mapdval4N  42466  mapdordlem1a  42468  aks4d1p8  42914  fimgmcyc  43362  prjsperref  43398  prjspeclsp  43404  elmzpcl  43517  mzpindd  43537  fphpd  43603  pw2f1ocnv  43824  islmodfg  43856  islssfg2  43858  dflim6  44051  onsucf1olem  44057  omge2  44085  tfsconcatlem  44123  tfsconcat0i  44132  rp-isfinite6  44304  minregex  44320  elmapintrab  44362  elinintrab  44363  relintab  44369  dfrtrcl5  44415  fsovrfovd  44795  ntrk1k3eqk13  44836  gneispace3  44919  k0004lem1  44933  pm13.192  45180  opelopab4  45320  ax6e2nd  45327  en3lplem2VD  45612  ax6e2ndVD  45676  ax6e2ndALT  45698  permaxrep  45775  iuneq1i  45864  ssrabf  45892  limcrecl  46405  dvnprodlem2  46721  fourierdlem103  46983  fourierdlem104  46984  4an21  48067  sprvalpwn0  48292  pairreueq  48319  dfvopnbgr2  48678  isubgredg  48691  xpsnopab  48982  sgrp2sgrp  49052  mpomptx2  49174  lindslinindsimp1  49296  lindslinindsimp2  49302  itsclc0b  49611  mo0sn  49653  coxp  49670  isthincd2  50274  thinccic  50308  2arwcatlem1  50432  setc1onsubc  50439  alsanmo  50647  ralsanmo  50648  alsralrex  50649  aacllem  50680