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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anbi2ci  626  anbi12i  628  bianassc  642  anandi  675  pm5.53  1004  dfifp4  1066  dfifp5  1067  3an4anass  1106  3ioran  1107  an6  1446  an3andi  1483  an33rean  1484  an33reanOLD  1485  19.26-3an  1876  19.28v  1995  sb3an  2085  19.28  2222  eeeanv  2347  sbel2x  2474  2eu4  2651  r19.26-3  3113  r19.41v  3189  3reeanv  3228  r19.41  3261  rexcomf  3301  cbvreuwOLD  3413  cbvreu  3425  rabeqi  3446  rabrabi  3451  rabrab  3456  ceqsex3v  3532  spc2ed  3592  rexabOLD  3692  rexrab  3693  reurab  3698  rmo4  3727  rmo3f  3731  reuind  3750  sbc3an  3848  rmo3  3884  ssrab  4071  rexun  4191  elin3  4201  inass  4220  rexin  4240  dfun2  4260  indifdirOLD  4286  difin2  4292  inrab2  4308  rabun2  4314  reuun2  4315  undif4  4467  rexdifpr  4662  rexsns  4674  rexdifsn  4798  2ralunsn  4896  iuncom4  5006  iindif1  5079  iunxiun  5101  disjxun  5147  zfrep4  5297  inuni  5344  reusv2lem4  5400  reusv2  5402  otth2  5484  copsexgw  5491  copsexg  5492  copsex2g  5494  copsex4g  5496  vopelopabsb  5530  otelxp  5721  rabxp  5725  opeliunxp  5744  xpundir  5746  xpiundi  5747  xpiundir  5748  brinxp2  5754  copsex2gb  5807  dminss  6153  imainss  6154  difxp  6164  cnvresima  6230  coundi  6247  resco  6250  imaco  6251  rnco  6252  coiun  6256  coi1  6262  coass  6265  cnvpo  6287  xpco  6289  dfpo2  6296  frpoind  6344  wfiOLD  6353  dffun2  6554  dffun2OLD  6555  dffun2OLDOLD  6556  fncnv  6622  imadif  6633  mptun  6697  ffrnb  6733  dff1o2  6839  dff1o3  6840  brprcneu  6882  brprcneuALT  6883  fvun2  6984  eqfnfv3  7035  respreima  7068  f1ompt  7111  f1ossf1o  7126  fsn  7133  fmptsng  7166  fmptsnd  7167  tpres  7202  abrexco  7243  imaiun  7244  f1mpt  7260  dff1o6  7273  imaeqsexv  7360  riotarab  7408  oprabidw  7440  oprabid  7441  dfoprab2  7467  oprab4  7495  mpomptx  7521  elpwpwel  7754  elxp4  7913  elxp5  7914  ffoss  7932  f11o  7933  opabex3d  7952  opabex3rd  7953  opabex3  7954  abexssex  7957  elxp7  8010  dfopab2  8038  dfoprab3s  8039  fsplit  8103  frxp  8112  xporderlem  8113  frpoins3xp3g  8127  soseq  8145  suppssov1  8183  suppssfv  8187  brtpos2  8217  tpostpos  8231  tposmpo  8248  wfrfunOLD  8319  dfrecs3  8372  dfrecs3OLD  8373  oarec  8562  oeeu  8603  eldifsucnn  8663  naddasslem1  8693  mapsncnv  8887  dfixp  8893  domen  8957  xpsnen  9055  xpcomco  9062  xpassen  9066  sbthlem9  9091  frfi  9288  marypha2lem2  9431  brttrcl2  9709  epfrs  9726  tcsni  9738  frind  9745  cp  9886  dfac5lem1  10118  dfac5lem2  10119  dfac5lem5  10122  kmlem3  10147  dfackm  10161  cfval2  10255  cflim3  10257  cfss  10260  cfslb  10261  zfcndrep  10609  eltsk2g  10746  ltexpi  10897  recmulnq  10959  ltexprlem4  11034  addsrpr  11070  mulsrpr  11071  addcnsr  11130  mulcnsr  11131  ltresr  11135  axrrecex  11158  elnnz  12568  elnn0z  12571  fnn0ind  12661  rexuz2  12883  rexrp  12995  elixx3g  13337  elfz2  13491  elfzuzb  13495  fznn  13569  elfz2nn0  13592  fznn0  13593  4fvwrd4  13621  preduz  13623  elfzo2  13635  fzind2  13750  hashgt23el  14384  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  fz1isolem  14422  s4f1o  14869  wwlktovfo  14909  fsum2dlem  15716  modfsummod  15740  sinltx  16132  divalglem10  16345  divalgb  16347  coprmproddvdslem  16599  isprm2  16619  infpn2  16846  prdsle  17408  prdsless  17409  prdsleval  17423  imasleval  17487  xpscf  17511  dfiso2  17719  oppcsect  17725  elhoma  17982  ispos2  18268  lubeldm  18306  glbeldm  18319  tosso  18372  ismhm  18673  issubm  18684  submacs  18708  issubg  19006  issubg3  19024  gaorb  19171  pmtrrn2  19328  efgcpbllema  19622  efgcpbllemb  19623  frgpuplem  19640  imasabl  19744  subgdmdprd  19904  dprd2d2  19914  dfrhm2  20253  issubrg  20319  drngprop  20372  drngid2  20378  opprdrng  20389  isabv  20427  islss  20545  islbs  20687  lsmspsn  20695  isobs  21275  islinds  21364  isassa  21411  aspval2  21452  ltbval  21598  opsrle  21602  opsrtoslem1  21616  fvmptnn04if  22351  ntreq0  22581  restntr  22686  cnnei  22786  hausnei2  22857  cmpcov2  22894  cmpsub  22904  uncmp  22907  cmpfi  22912  llyi  22978  dissnlocfin  23033  iskgen3  23053  1stckgenlem  23057  ptpjpre1  23075  txcnpi  23112  txtube  23144  hausdiag  23149  txlm  23152  txkgen  23156  cfinfil  23397  csdfil  23398  supfil  23399  fin1aufil  23436  elflim2  23468  hauspwpwf1  23491  txflf  23510  isfcls  23513  alexsubALTlem3  23553  alexsubALT  23555  cnextcn  23571  istmd  23578  istgp  23581  tgphaus  23621  qustgplem  23625  istrg  23668  istdrg  23670  istlm  23689  blres  23937  isms2  23956  metrest  24033  metuel2  24074  restmetu  24079  isngp  24105  isnlm  24192  elii1  24451  isclmp  24613  iscvsp  24644  isncvsngp  24666  iscph  24687  cfilucfil3  24837  isbn  24855  limcrcl  25391  ig1pval3  25692  plydivex  25810  ellogdm  26147  cubic  26354  dmarea  26462  vmasum  26719  lgsquadlem1  26883  lgsquadlem2  26884  elno3  27158  slenlt  27255  madeval2  27348  istrkg3ld  27712  legov  27836  ltgov  27848  colinearalg  28168  axeuclid  28221  axcontlem2  28223  axcontlem5  28226  nbgrel  28597  nbupgrres  28621  nbusgredgeu0  28625  nb3grprlem2  28638  nb3grpr2  28640  nb3gr2nb  28641  cplgr3v  28692  finsumvtxdg2ssteplem3  28804  wlkonprop  28915  upgrtrls  28958  upgristrl  28959  wksonproplem  28961  wksonproplemOLD  28962  usgr2pth0  29022  wwlksnext  29147  wwlksnextsurj  29154  wwlksnfi  29160  wspthsnwspthsnon  29170  wpthswwlks2on  29215  rusgrnumwwlkl1  29222  erclwwlkref  29273  isclwwlknx  29289  clwwlknwwlksn  29291  clwwlkel  29299  erclwwlknref  29322  clwlknf1oclwwlkn  29337  clwwlknonel  29348  clwwlknon1  29350  clwwlknon2x  29356  clwwlkvbij  29366  iseupthf1o  29455  2pthfrgrrn  29535  fusgr2wsp2nb  29587  numclwwlk1lem2f1  29610  numclwwlkovh  29626  numclwlk2lem2f1o  29632  frgrregord013  29648  avril1  29716  islno  30006  h2hlm  30233  hcau  30437  hhsssh2  30523  dfch2  30660  elcnop  31110  ellnop  31111  elhmop  31126  elcnfn  31135  ellnfn  31136  dmadjss  31140  adjeu  31142  adjval  31143  hhcno  31157  hhcnf  31158  eleigvec  31210  isst  31466  ishst  31467  cvnbtwn3  31541  cvnbtwn4  31542  chirredi  31647  sumdmdii  31668  or3di  31701  rexunirn  31732  rmoun  31734  dmrab  31737  difrab2  31738  iunin1f  31789  disjunsn  31825  opeldifid  31830  ofpreima  31890  mpomptxf  31905  1stpreima  31928  2ndpreima  31929  f1od2  31946  resf1o  31955  maprnin  31956  nndiffz1  31997  ismnt  32153  mgcval  32157  omndmul2  32230  isorng  32417  opprnsg  32598  smatrcl  32776  ordtconnlem1  32904  isrrext  32980  sigaex  33108  sigaval  33109  omssubaddlem  33298  omssubadd  33299  eulerpartleme  33362  eulerpartlemt0  33368  eulerpartlemr  33373  eulerpartlemn  33380  probun  33418  ballotlemelo  33486  ballotlem2  33487  ballotlemfc0  33491  ballotlemfcc  33492  reprdifc  33639  bnj248  33711  bnj250  33712  bnj268  33720  bnj312  33723  bnj945  33784  bnj110  33869  bnj849  33936  bnj882  33937  bnj893  33939  bnj916  33944  bnj983  33962  bnj1040  33983  bnj1175  34015  cusgredgex  34112  cusgr3cyclex  34127  erdszelem1  34182  iscvm  34250  elmpst  34527  mpstrcl  34532  dfso3  34689  xpab  34695  coepr  34723  dfdm5  34744  dfrn5  34745  elima4  34747  fv1stcnv  34748  fv2ndcnv  34749  brpprod  34857  dfon3  34864  elfix  34875  dffix2  34877  elfuns  34887  brimg  34909  brapply  34910  brsuccf  34913  funpartlem  34914  funpartfun  34915  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  lineunray  35119  ellines  35124  finminlem  35203  fneval  35237  neibastop3  35247  eliminable-abelv  35748  bj-inrab  35807  bj-rest10  35969  bj-restpw  35973  bj-restuni  35978  bj-mpomptALT  36000  bj-imdirco  36071  icorempo  36232  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlpssretop  36245  pibt2  36298  wl-ifp-ncond2  36346  wl-df3-3mintru2  36367  wl-2mintru1  36371  rabiun  36461  iundif1  36462  lindsenlbs  36483  poimirlem4  36492  poimirlem25  36513  poimirlem26  36514  poimirlem29  36517  poimirlem30  36518  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  ftc1anc  36569  isbnd2  36651  bndss  36654  heibor1lem  36677  heibor1  36678  isrngohom  36833  isidl  36882  sbccom2lem  36992  anan  37093  bianbi  37095  eqbrb  37099  eqelb  37101  br1cnvinxp  37124  eldmqsres  37155  idinxpssinxp2  37187  moantr  37233  inxpxrn  37265  dfcoss3  37284  cocossss  37306  ressn2  37312  br1cossinidres  37319  br1cossincnvepres  37320  br1cossxrnidres  37321  br1cossxrncnvepres  37322  refrelcoss2  37334  symrelcoss2  37336  cosscnvssid5  37348  br1cossxrncnvssrres  37378  dfrefrel3  37386  dfcnvrefrel3  37401  cosselcnvrefrels2  37408  cosselcnvrefrels3  37409  cosselcnvrefrels4  37410  cosselcnvrefrels5  37411  dfsymrel3  37420  refsymrel2  37437  refsymrel3  37438  elrefsymrels3  37440  dftrrel3  37448  dfeqvrel2  37460  dfeqvrel3  37461  redundpbi1  37501  refrelredund3  37507  eldmqs1cossres  37529  dffunALTV2  37558  dffunALTV3  37559  dffunALTV4  37560  dffunALTV5  37561  dfdisjALTV  37583  dfdisjALTV2  37584  dfdisjALTV3  37585  dfdisjALTV4  37586  eldisjs3  37594  eldisjs4  37595  disjsuc  37629  prtlem70  37727  prtlem100  37729  prter2  37751  lsateln0  37865  islshpat  37887  lcvnbtwn3  37898  islfl  37930  ishlat1  38222  ishlat2  38223  cvrat4  38314  islvol5  38450  psubspset  38615  snatpsubN  38621  dalawlem13  38754  psubclsetN  38807  isltrn2N  38991  cdlemftr3  39436  dibelval3  40018  dicval2  40050  dicopelval2  40052  dicelval2N  40053  dihglb2  40213  islpolN  40354  lcfls1c  40407  mapdvalc  40500  mapdval4N  40503  mapdordlem1a  40505  aks4d1p8  40952  prjsperref  41348  prjspeclsp  41354  elmzpcl  41464  mzpindd  41484  fphpd  41554  pw2f1ocnv  41776  islmodfg  41811  islssfg2  41813  isdomn3  41946  dflim6  42014  onsucf1olem  42020  omge2  42048  tfsconcatlem  42086  tfsconcat0i  42095  rp-isfinite6  42269  minregex  42285  elmapintrab  42327  elinintrab  42328  relintab  42334  dfrtrcl5  42380  fsovrfovd  42760  ntrk1k3eqk13  42801  gneispace3  42884  k0004lem1  42898  pm13.192  43169  opelopab4  43312  ax6e2nd  43319  en3lplem2VD  43605  ax6e2ndVD  43669  ax6e2ndALT  43691  ssrabf  43803  limcrecl  44345  dvnprodlem2  44663  fourierdlem103  44925  fourierdlem104  44926  4an21  45978  sprvalpwn0  46151  pairreueq  46178  xpsnopab  46535  ismgmhm  46553  issubmgm  46559  submgmacs  46574  sgrp2sgrp  46638  opeliun2xp  47008  mpomptx2  47010  lindslinindsimp1  47138  lindslinindsimp2  47144  itsclc0b  47458  mo0sn  47500  iscnrm3lem3  47568  isthincd2  47658  thinccic  47681  alsconv  47837  aacllem  47848