Theorem anbi1i 622

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  anbi2ci  623  anbi12i  625  bianassc  639  anandi  672  pm5.53  1001  dfifp4  1063  dfifp5  1064  3an4anass  1103  3ioran  1104  an6  1443  an3andi  1480  an33rean  1481  an33reanOLD  1482  19.26-3an  1873  19.28v  1992  sb3an  2082  19.28  2219  eeeanv  2344  sbel2x  2471  2eu4  2648  r19.26-3  3110  r19.41v  3186  3reeanv  3225  r19.41  3258  rexcomf  3298  cbvreuwOLD  3410  cbvreu  3422  rabeqi  3443  rabrabi  3448  rabrab  3453  ceqsex3v  3530  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  7113  f1ossf1o  7129  fsn  7136  fmptsng  7169  fmptsnd  7170  tpres  7205  abrexco  7247  imaiun  7248  f1mpt  7264  dff1o6  7277  imaeqsexv  7364  riotarab  7412  oprabidw  7444  oprabid  7445  dfoprab2  7471  oprab4  7499  mpomptx  7525  elpwpwel  7758  elxp4  7917  elxp5  7918  ffoss  7936  f11o  7937  opabex3d  7956  opabex3rd  7957  opabex3  7958  abexssex  7961  elxp7  8014  dfopab2  8042  dfoprab3s  8043  fsplit  8107  frxp  8116  xporderlem  8117  frpoins3xp3g  8131  soseq  8149  suppssov1  8187  suppssfv  8191  brtpos2  8221  tpostpos  8235  tposmpo  8252  wfrfunOLD  8323  dfrecs3  8376  dfrecs3OLD  8377  oarec  8566  oeeu  8607  eldifsucnn  8667  naddasslem1  8697  mapsncnv  8891  dfixp  8897  domen  8961  xpsnen  9059  xpcomco  9066  xpassen  9070  sbthlem9  9095  frfi  9292  marypha2lem2  9435  brttrcl2  9713  epfrs  9730  tcsni  9742  frind  9749  cp  9890  dfac5lem1  10122  dfac5lem2  10123  dfac5lem5  10126  kmlem3  10151  dfackm  10165  cfval2  10259  cflim3  10261  cfss  10264  cfslb  10265  zfcndrep  10613  eltsk2g  10750  ltexpi  10901  recmulnq  10963  ltexprlem4  11038  addsrpr  11074  mulsrpr  11075  addcnsr  11134  mulcnsr  11135  ltresr  11139  axrrecex  11162  elnnz  12574  elnn0z  12577  fnn0ind  12667  rexuz2  12889  rexrp  13001  elixx3g  13343  elfz2  13497  elfzuzb  13501  fznn  13575  elfz2nn0  13598  fznn0  13599  4fvwrd4  13627  preduz  13629  elfzo2  13641  fzind2  13756  hashgt23el  14390  hashf1lem1  14421  hashf1lem1OLD  14422  hashf1lem2  14423  fz1isolem  14428  s4f1o  14875  wwlktovfo  14915  fsum2dlem  15722  modfsummod  15746  sinltx  16138  divalglem10  16351  divalgb  16353  coprmproddvdslem  16605  isprm2  16625  infpn2  16852  prdsle  17414  prdsless  17415  prdsleval  17429  imasleval  17493  xpscf  17517  dfiso2  17725  oppcsect  17731  elhoma  17988  ispos2  18274  lubeldm  18312  glbeldm  18325  tosso  18378  ismgmhm  18623  issubmgm  18629  submgmacs  18644  ismhm  18709  issubm  18722  submacs  18746  issubg  19044  issubg3  19062  gaorb  19214  pmtrrn2  19371  efgcpbllema  19665  efgcpbllemb  19666  frgpuplem  19683  imasabl  19787  subgdmdprd  19947  dprd2d2  19957  dfrhm2  20367  issubrg  20463  drngprop  20517  drngid2  20523  opprdrng  20534  isabv  20572  islss  20691  islbs  20833  lsmspsn  20841  isobs  21496  islinds  21585  isassa  21632  aspval2  21673  ltbval  21819  opsrle  21823  opsrtoslem1  21837  fvmptnn04if  22573  ntreq0  22803  restntr  22908  cnnei  23008  hausnei2  23079  cmpcov2  23116  cmpsub  23126  uncmp  23129  cmpfi  23134  llyi  23200  dissnlocfin  23255  iskgen3  23275  1stckgenlem  23279  ptpjpre1  23297  txcnpi  23334  txtube  23366  hausdiag  23371  txlm  23374  txkgen  23378  cfinfil  23619  csdfil  23620  supfil  23621  fin1aufil  23658  elflim2  23690  hauspwpwf1  23713  txflf  23732  isfcls  23735  alexsubALTlem3  23775  alexsubALT  23777  cnextcn  23793  istmd  23800  istgp  23803  tgphaus  23843  qustgplem  23847  istrg  23890  istdrg  23892  istlm  23911  blres  24159  isms2  24178  metrest  24255  metuel2  24296  restmetu  24301  isngp  24327  isnlm  24414  elii1  24680  isclmp  24846  iscvsp  24877  isncvsngp  24899  iscph  24920  cfilucfil3  25070  isbn  25088  limcrcl  25625  ig1pval3  25926  plydivex  26044  ellogdm  26381  cubic  26588  dmarea  26696  vmasum  26953  lgsquadlem1  27117  lgsquadlem2  27118  elno3  27392  slenlt  27489  madeval2  27583  istrkg3ld  27977  legov  28101  ltgov  28113  colinearalg  28433  axeuclid  28486  axcontlem2  28488  axcontlem5  28491  nbgrel  28862  nbupgrres  28886  nbusgredgeu0  28890  nb3grprlem2  28903  nb3grpr2  28905  nb3gr2nb  28906  cplgr3v  28957  finsumvtxdg2ssteplem3  29069  wlkonprop  29180  upgrtrls  29223  upgristrl  29224  wksonproplem  29226  wksonproplemOLD  29227  usgr2pth0  29287  wwlksnext  29412  wwlksnextsurj  29419  wwlksnfi  29425  wspthsnwspthsnon  29435  wpthswwlks2on  29480  rusgrnumwwlkl1  29487  erclwwlkref  29538  isclwwlknx  29554  clwwlknwwlksn  29556  clwwlkel  29564  erclwwlknref  29587  clwlknf1oclwwlkn  29602  clwwlknonel  29613  clwwlknon1  29615  clwwlknon2x  29621  clwwlkvbij  29631  iseupthf1o  29720  2pthfrgrrn  29800  fusgr2wsp2nb  29852  numclwwlk1lem2f1  29875  numclwwlkovh  29891  numclwlk2lem2f1o  29897  frgrregord013  29913  avril1  29981  islno  30271  h2hlm  30498  hcau  30702  hhsssh2  30788  dfch2  30925  elcnop  31375  ellnop  31376  elhmop  31391  elcnfn  31400  ellnfn  31401  dmadjss  31405  adjeu  31407  adjval  31408  hhcno  31422  hhcnf  31423  eleigvec  31475  isst  31731  ishst  31732  cvnbtwn3  31806  cvnbtwn4  31807  chirredi  31912  sumdmdii  31933  or3di  31966  rexunirn  31997  rmoun  31999  dmrab  32002  difrab2  32003  iunin1f  32054  disjunsn  32090  opeldifid  32095  ofpreima  32155  mpomptxf  32170  1stpreima  32193  2ndpreima  32194  f1od2  32211  resf1o  32220  maprnin  32221  nndiffz1  32262  ismnt  32418  mgcval  32422  omndmul2  32498  isorng  32685  opprnsg  32870  smatrcl  33072  ordtconnlem1  33200  isrrext  33276  sigaex  33404  sigaval  33405  omssubaddlem  33594  omssubadd  33595  eulerpartleme  33658  eulerpartlemt0  33664  eulerpartlemr  33669  eulerpartlemn  33676  probun  33714  ballotlemelo  33782  ballotlem2  33783  ballotlemfc0  33787  ballotlemfcc  33788  reprdifc  33935  bnj248  34007  bnj250  34008  bnj268  34016  bnj312  34019  bnj945  34080  bnj110  34165  bnj849  34232  bnj882  34233  bnj893  34235  bnj916  34240  bnj983  34258  bnj1040  34279  bnj1175  34311  cusgredgex  34408  cusgr3cyclex  34423  erdszelem1  34478  iscvm  34546  elmpst  34823  mpstrcl  34828  dfso3  34991  xpab  34997  coepr  35025  dfdm5  35046  dfrn5  35047  elima4  35049  fv1stcnv  35050  fv2ndcnv  35051  brpprod  35159  dfon3  35166  elfix  35177  dffix2  35179  elfuns  35189  brimg  35211  brapply  35212  brsuccf  35215  funpartlem  35216  funpartfun  35217  brrestrict  35223  dfrecs2  35224  dfrdg4  35225  lineunray  35421  ellines  35426  finminlem  35508  fneval  35542  neibastop3  35552  eliminable-abelv  36053  bj-inrab  36112  bj-rest10  36274  bj-restpw  36278  bj-restuni  36283  bj-mpomptALT  36305  bj-imdirco  36376  icorempo  36537  isbasisrelowllem1  36541  isbasisrelowllem2  36542  relowlpssretop  36550  pibt2  36603  wl-ifp-ncond2  36651  wl-df3-3mintru2  36672  wl-2mintru1  36676  rabiun  36766  iundif1  36767  lindsenlbs  36788  poimirlem4  36797  poimirlem25  36818  poimirlem26  36819  poimirlem29  36822  poimirlem30  36823  ismblfin  36834  ovoliunnfl  36835  voliunnfl  36837  volsupnfl  36838  itg2addnclem2  36845  itg2addnclem3  36846  itg2addnc  36847  ftc1anc  36874  isbnd2  36956  bndss  36959  heibor1lem  36982  heibor1  36983  isrngohom  37138  isidl  37187  sbccom2lem  37297  anan  37398  bianbi  37400  eqbrb  37404  eqelb  37406  br1cnvinxp  37429  eldmqsres  37460  idinxpssinxp2  37492  moantr  37538  inxpxrn  37570  dfcoss3  37589  cocossss  37611  ressn2  37617  br1cossinidres  37624  br1cossincnvepres  37625  br1cossxrnidres  37626  br1cossxrncnvepres  37627  refrelcoss2  37639  symrelcoss2  37641  cosscnvssid5  37653  br1cossxrncnvssrres  37683  dfrefrel3  37691  dfcnvrefrel3  37706  cosselcnvrefrels2  37713  cosselcnvrefrels3  37714  cosselcnvrefrels4  37715  cosselcnvrefrels5  37716  dfsymrel3  37725  refsymrel2  37742  refsymrel3  37743  elrefsymrels3  37745  dftrrel3  37753  dfeqvrel2  37765  dfeqvrel3  37766  redundpbi1  37806  refrelredund3  37812  eldmqs1cossres  37834  dffunALTV2  37863  dffunALTV3  37864  dffunALTV4  37865  dffunALTV5  37866  dfdisjALTV  37888  dfdisjALTV2  37889  dfdisjALTV3  37890  dfdisjALTV4  37891  eldisjs3  37899  eldisjs4  37900  disjsuc  37934  prtlem70  38032  prtlem100  38034  prter2  38056  lsateln0  38170  islshpat  38192  lcvnbtwn3  38203  islfl  38235  ishlat1  38527  ishlat2  38528  cvrat4  38619  islvol5  38755  psubspset  38920  snatpsubN  38926  dalawlem13  39059  psubclsetN  39112  isltrn2N  39296  cdlemftr3  39741  dibelval3  40323  dicval2  40355  dicopelval2  40357  dicelval2N  40358  dihglb2  40518  islpolN  40659  lcfls1c  40712  mapdvalc  40805  mapdval4N  40808  mapdordlem1a  40810  aks4d1p8  41260  prjsperref  41652  prjspeclsp  41658  elmzpcl  41768  mzpindd  41788  fphpd  41858  pw2f1ocnv  42080  islmodfg  42115  islssfg2  42117  isdomn3  42250  dflim6  42318  onsucf1olem  42324  omge2  42352  tfsconcatlem  42390  tfsconcat0i  42399  rp-isfinite6  42573  minregex  42589  elmapintrab  42631  elinintrab  42632  relintab  42638  dfrtrcl5  42684  fsovrfovd  43064  ntrk1k3eqk13  43105  gneispace3  43188  k0004lem1  43202  pm13.192  43473  opelopab4  43616  ax6e2nd  43623  en3lplem2VD  43909  ax6e2ndVD  43973  ax6e2ndALT  43995  ssrabf  44106  limcrecl  44645  dvnprodlem2  44963  fourierdlem103  45225  fourierdlem104  45226  4an21  46278  sprvalpwn0  46451  pairreueq  46478  xpsnopab  46835  sgrp2sgrp  46906  opeliun2xp  47098  mpomptx2  47100  lindslinindsimp1  47227  lindslinindsimp2  47233  itsclc0b  47547  mo0sn  47589  iscnrm3lem3  47657  isthincd2  47747  thinccic  47770  alsconv  47926  aacllem  47937