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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anbi2ci  625  anbi12i  627  bianassc  641  anandi  674  pm5.53  1003  dfifp4  1065  dfifp5  1066  3an4anass  1105  3ioran  1106  an6  1445  an3andi  1482  an33rean  1483  an33reanOLD  1484  19.26-3an  1875  19.28v  1994  sb3an  2084  19.28  2221  eeeanv  2346  sbel2x  2473  2eu4  2650  r19.26-3  3112  r19.41v  3188  3reeanv  3227  r19.41  3260  rexcomf  3300  cbvreuwOLD  3412  cbvreu  3424  rabeqi  3445  rabrabi  3450  rabrab  3455  ceqsex3v  3531  spc2ed  3591  rexabOLD  3690  rexrab  3691  reurab  3696  rmo4  3725  rmo3f  3729  reuind  3748  sbc3an  3846  rmo3  3882  ssrab  4069  rexun  4189  elin3  4199  inass  4218  rexin  4238  dfun2  4258  indifdirOLD  4284  difin2  4290  inrab2  4306  rabun2  4312  reuun2  4313  undif4  4465  rexdifpr  4660  rexsns  4672  rexdifsn  4796  2ralunsn  4894  iuncom4  5004  iindif1  5077  iunxiun  5099  disjxun  5145  zfrep4  5295  inuni  5342  reusv2lem4  5398  reusv2  5400  otth2  5482  copsexgw  5489  copsexg  5490  copsex2g  5492  copsex4g  5494  vopelopabsb  5528  otelxp  5718  rabxp  5722  opeliunxp  5741  xpundir  5743  xpiundi  5744  xpiundir  5745  brinxp2  5751  copsex2gb  5804  dminss  6149  imainss  6150  difxp  6160  cnvresima  6226  coundi  6243  resco  6246  imaco  6247  rnco  6248  coiun  6252  coi1  6258  coass  6261  cnvpo  6283  xpco  6285  dfpo2  6292  frpoind  6340  wfiOLD  6349  dffun2  6550  dffun2OLD  6551  dffun2OLDOLD  6552  fncnv  6618  imadif  6629  mptun  6693  ffrnb  6729  dff1o2  6835  dff1o3  6836  brprcneu  6878  brprcneuALT  6879  fvun2  6980  eqfnfv3  7031  respreima  7064  f1ompt  7107  f1ossf1o  7122  fsn  7129  fmptsng  7162  fmptsnd  7163  tpres  7198  abrexco  7239  imaiun  7240  f1mpt  7256  dff1o6  7269  imaeqsexv  7356  riotarab  7404  oprabidw  7436  oprabid  7437  dfoprab2  7463  oprab4  7491  mpomptx  7517  elpwpwel  7750  elxp4  7909  elxp5  7910  ffoss  7928  f11o  7929  opabex3d  7948  opabex3rd  7949  opabex3  7950  abexssex  7953  elxp7  8006  dfopab2  8034  dfoprab3s  8035  fsplit  8099  frxp  8108  xporderlem  8109  frpoins3xp3g  8123  soseq  8141  suppssov1  8179  suppssfv  8183  brtpos2  8213  tpostpos  8227  tposmpo  8244  wfrfunOLD  8315  dfrecs3  8368  dfrecs3OLD  8369  oarec  8558  oeeu  8599  eldifsucnn  8659  naddasslem1  8689  mapsncnv  8883  dfixp  8889  domen  8953  xpsnen  9051  xpcomco  9058  xpassen  9062  sbthlem9  9087  frfi  9284  marypha2lem2  9427  brttrcl2  9705  epfrs  9722  tcsni  9734  frind  9741  cp  9882  dfac5lem1  10114  dfac5lem2  10115  dfac5lem5  10118  kmlem3  10143  dfackm  10157  cfval2  10251  cflim3  10253  cfss  10256  cfslb  10257  zfcndrep  10605  eltsk2g  10742  ltexpi  10893  recmulnq  10955  ltexprlem4  11030  addsrpr  11066  mulsrpr  11067  addcnsr  11126  mulcnsr  11127  ltresr  11131  axrrecex  11154  elnnz  12564  elnn0z  12567  fnn0ind  12657  rexuz2  12879  rexrp  12991  elixx3g  13333  elfz2  13487  elfzuzb  13491  fznn  13565  elfz2nn0  13588  fznn0  13589  4fvwrd4  13617  preduz  13619  elfzo2  13631  fzind2  13746  hashgt23el  14380  hashf1lem1  14411  hashf1lem1OLD  14412  hashf1lem2  14413  fz1isolem  14418  s4f1o  14865  wwlktovfo  14905  fsum2dlem  15712  modfsummod  15736  sinltx  16128  divalglem10  16341  divalgb  16343  coprmproddvdslem  16595  isprm2  16615  infpn2  16842  prdsle  17404  prdsless  17405  prdsleval  17419  imasleval  17483  xpscf  17507  dfiso2  17715  oppcsect  17721  elhoma  17978  ispos2  18264  lubeldm  18302  glbeldm  18315  tosso  18368  ismhm  18669  issubm  18680  submacs  18704  issubg  19000  issubg3  19018  gaorb  19165  pmtrrn2  19322  efgcpbllema  19616  efgcpbllemb  19617  frgpuplem  19634  imasabl  19738  subgdmdprd  19898  dprd2d2  19908  dfrhm2  20245  drngprop  20322  drngid2  20328  opprdrng  20339  issubrg  20355  isabv  20419  islss  20537  islbs  20679  lsmspsn  20687  isobs  21266  islinds  21355  isassa  21402  aspval2  21443  ltbval  21589  opsrle  21593  opsrtoslem1  21607  fvmptnn04if  22342  ntreq0  22572  restntr  22677  cnnei  22777  hausnei2  22848  cmpcov2  22885  cmpsub  22895  uncmp  22898  cmpfi  22903  llyi  22969  dissnlocfin  23024  iskgen3  23044  1stckgenlem  23048  ptpjpre1  23066  txcnpi  23103  txtube  23135  hausdiag  23140  txlm  23143  txkgen  23147  cfinfil  23388  csdfil  23389  supfil  23390  fin1aufil  23427  elflim2  23459  hauspwpwf1  23482  txflf  23501  isfcls  23504  alexsubALTlem3  23544  alexsubALT  23546  cnextcn  23562  istmd  23569  istgp  23572  tgphaus  23612  qustgplem  23616  istrg  23659  istdrg  23661  istlm  23680  blres  23928  isms2  23947  metrest  24024  metuel2  24065  restmetu  24070  isngp  24096  isnlm  24183  elii1  24442  isclmp  24604  iscvsp  24635  isncvsngp  24657  iscph  24678  cfilucfil3  24828  isbn  24846  limcrcl  25382  ig1pval3  25683  plydivex  25801  ellogdm  26138  cubic  26343  dmarea  26451  vmasum  26708  lgsquadlem1  26872  lgsquadlem2  26873  elno3  27147  slenlt  27244  madeval2  27337  istrkg3ld  27701  legov  27825  ltgov  27837  colinearalg  28157  axeuclid  28210  axcontlem2  28212  axcontlem5  28215  nbgrel  28586  nbupgrres  28610  nbusgredgeu0  28614  nb3grprlem2  28627  nb3grpr2  28629  nb3gr2nb  28630  cplgr3v  28681  finsumvtxdg2ssteplem3  28793  wlkonprop  28904  upgrtrls  28947  upgristrl  28948  wksonproplem  28950  wksonproplemOLD  28951  usgr2pth0  29011  wwlksnext  29136  wwlksnextsurj  29143  wwlksnfi  29149  wspthsnwspthsnon  29159  wpthswwlks2on  29204  rusgrnumwwlkl1  29211  erclwwlkref  29262  isclwwlknx  29278  clwwlknwwlksn  29280  clwwlkel  29288  erclwwlknref  29311  clwlknf1oclwwlkn  29326  clwwlknonel  29337  clwwlknon1  29339  clwwlknon2x  29345  clwwlkvbij  29355  iseupthf1o  29444  2pthfrgrrn  29524  fusgr2wsp2nb  29576  numclwwlk1lem2f1  29599  numclwwlkovh  29615  numclwlk2lem2f1o  29621  frgrregord013  29637  avril1  29705  islno  29993  h2hlm  30220  hcau  30424  hhsssh2  30510  dfch2  30647  elcnop  31097  ellnop  31098  elhmop  31113  elcnfn  31122  ellnfn  31123  dmadjss  31127  adjeu  31129  adjval  31130  hhcno  31144  hhcnf  31145  eleigvec  31197  isst  31453  ishst  31454  cvnbtwn3  31528  cvnbtwn4  31529  chirredi  31634  sumdmdii  31655  or3di  31688  rexunirn  31719  rmoun  31721  dmrab  31724  difrab2  31725  iunin1f  31776  disjunsn  31812  opeldifid  31817  ofpreima  31877  mpomptxf  31892  1stpreima  31915  2ndpreima  31916  f1od2  31933  resf1o  31942  maprnin  31943  nndiffz1  31984  ismnt  32140  mgcval  32144  omndmul2  32217  isorng  32405  opprnsg  32586  smatrcl  32764  ordtconnlem1  32892  isrrext  32968  sigaex  33096  sigaval  33097  omssubaddlem  33286  omssubadd  33287  eulerpartleme  33350  eulerpartlemt0  33356  eulerpartlemr  33361  eulerpartlemn  33368  probun  33406  ballotlemelo  33474  ballotlem2  33475  ballotlemfc0  33479  ballotlemfcc  33480  reprdifc  33627  bnj248  33699  bnj250  33700  bnj268  33708  bnj312  33711  bnj945  33772  bnj110  33857  bnj849  33924  bnj882  33925  bnj893  33927  bnj916  33932  bnj983  33950  bnj1040  33971  bnj1175  34003  cusgredgex  34100  cusgr3cyclex  34115  erdszelem1  34170  iscvm  34238  elmpst  34515  mpstrcl  34520  dfso3  34677  xpab  34683  coepr  34711  dfdm5  34732  dfrn5  34733  elima4  34735  fv1stcnv  34736  fv2ndcnv  34737  brpprod  34845  dfon3  34852  elfix  34863  dffix2  34865  elfuns  34875  brimg  34897  brapply  34898  brsuccf  34901  funpartlem  34902  funpartfun  34903  brrestrict  34909  dfrecs2  34910  dfrdg4  34911  lineunray  35107  ellines  35112  finminlem  35191  fneval  35225  neibastop3  35235  eliminable-abelv  35736  bj-inrab  35795  bj-rest10  35957  bj-restpw  35961  bj-restuni  35966  bj-mpomptALT  35988  bj-imdirco  36059  icorempo  36220  isbasisrelowllem1  36224  isbasisrelowllem2  36225  relowlpssretop  36233  pibt2  36286  wl-ifp-ncond2  36334  wl-df3-3mintru2  36355  wl-2mintru1  36359  rabiun  36449  iundif1  36450  lindsenlbs  36471  poimirlem4  36480  poimirlem25  36501  poimirlem26  36502  poimirlem29  36505  poimirlem30  36506  ismblfin  36517  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  itg2addnclem2  36528  itg2addnclem3  36529  itg2addnc  36530  ftc1anc  36557  isbnd2  36639  bndss  36642  heibor1lem  36665  heibor1  36666  isrngohom  36821  isidl  36870  sbccom2lem  36980  anan  37081  bianbi  37083  eqbrb  37087  eqelb  37089  br1cnvinxp  37112  eldmqsres  37143  idinxpssinxp2  37175  moantr  37221  inxpxrn  37253  dfcoss3  37272  cocossss  37294  ressn2  37300  br1cossinidres  37307  br1cossincnvepres  37308  br1cossxrnidres  37309  br1cossxrncnvepres  37310  refrelcoss2  37322  symrelcoss2  37324  cosscnvssid5  37336  br1cossxrncnvssrres  37366  dfrefrel3  37374  dfcnvrefrel3  37389  cosselcnvrefrels2  37396  cosselcnvrefrels3  37397  cosselcnvrefrels4  37398  cosselcnvrefrels5  37399  dfsymrel3  37408  refsymrel2  37425  refsymrel3  37426  elrefsymrels3  37428  dftrrel3  37436  dfeqvrel2  37448  dfeqvrel3  37449  redundpbi1  37489  refrelredund3  37495  eldmqs1cossres  37517  dffunALTV2  37546  dffunALTV3  37547  dffunALTV4  37548  dffunALTV5  37549  dfdisjALTV  37571  dfdisjALTV2  37572  dfdisjALTV3  37573  dfdisjALTV4  37574  eldisjs3  37582  eldisjs4  37583  disjsuc  37617  prtlem70  37715  prtlem100  37717  prter2  37739  lsateln0  37853  islshpat  37875  lcvnbtwn3  37886  islfl  37918  ishlat1  38210  ishlat2  38211  cvrat4  38302  islvol5  38438  psubspset  38603  snatpsubN  38609  dalawlem13  38742  psubclsetN  38795  isltrn2N  38979  cdlemftr3  39424  dibelval3  40006  dicval2  40038  dicopelval2  40040  dicelval2N  40041  dihglb2  40201  islpolN  40342  lcfls1c  40395  mapdvalc  40488  mapdval4N  40491  mapdordlem1a  40493  aks4d1p8  40940  prjsperref  41344  prjspeclsp  41350  elmzpcl  41449  mzpindd  41469  fphpd  41539  pw2f1ocnv  41761  islmodfg  41796  islssfg2  41798  isdomn3  41931  dflim6  41999  onsucf1olem  42005  omge2  42033  tfsconcatlem  42071  tfsconcat0i  42080  rp-isfinite6  42254  minregex  42270  elmapintrab  42312  elinintrab  42313  relintab  42319  dfrtrcl5  42365  fsovrfovd  42745  ntrk1k3eqk13  42786  gneispace3  42869  k0004lem1  42883  pm13.192  43154  opelopab4  43297  ax6e2nd  43304  en3lplem2VD  43590  ax6e2ndVD  43654  ax6e2ndALT  43676  ssrabf  43788  limcrecl  44331  dvnprodlem2  44649  fourierdlem103  44911  fourierdlem104  44912  4an21  45964  sprvalpwn0  46137  pairreueq  46164  xpsnopab  46521  ismgmhm  46539  issubmgm  46545  submgmacs  46560  sgrp2sgrp  46624  opeliun2xp  46961  mpomptx2  46963  lindslinindsimp1  47091  lindslinindsimp2  47097  itsclc0b  47411  mo0sn  47453  iscnrm3lem3  47521  isthincd2  47611  thinccic  47634  alsconv  47790  aacllem  47801