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  19.26-3an  1872  sb3an  2081  eeeanv  2351  sbel2x  2478  rexcomf  3283  cbvreuwOLD  3394  cbvreu  3407  rabeqi  3429  rabrabi  3435  rabrab  3440  ceqsex3v  3516  spc2ed  3580  rexrab  3679  reurab  3684  rmo3f  3717  reuind  3736  rmo3  3864  ssrab  4048  rexun  4171  elin3  4181  inass  4203  rexin  4225  dfun2  4245  inrab2  4292  rabun2  4299  reuun2  4300  undif4  4442  rexdifpr  4635  rexsns  4647  rexdifsn  4770  2ralunsn  4871  iuncom4  4976  iindif1  5051  iunxiun  5073  disjxun  5117  zfrep4  5263  inuni  5320  reusv2lem4  5371  reusv2  5373  otth2  5458  copsexgw  5465  copsexg  5466  copsex2g  5468  copsex4g  5470  vopelopabsb  5504  rabxp  5702  opeliunxp  5721  opeliun2xp  5722  xpundir  5724  xpiundi  5725  xpiundir  5726  brinxp2  5732  copsex2gb  5785  cnvopab  6126  dminss  6142  imainss  6143  difxp  6153  cnvresima  6219  coundi  6236  resco  6239  imaco  6240  rnco  6241  coiun  6245  coi1  6251  coass  6254  cnvpo  6276  xpco  6278  dfpo2  6285  frpoind  6331  wfiOLD  6340  dffun2  6540  dffun2OLD  6541  dffun2OLDOLD  6542  fncnv  6608  imadif  6619  mptun  6683  ffrnb  6719  dff1o2  6822  dff1o3  6823  brprcneu  6865  brprcneuALT  6866  fvun2  6970  eqfnfv3  7022  respreima  7055  f1ompt  7100  f1ossf1o  7117  fsn  7124  fmptsng  7159  fmptsnd  7160  tpres  7192  abrexco  7235  imaiun  7236  f1mpt  7253  dff1o6  7267  imaeqsexvOLD  7355  riotarab  7402  oprabidw  7434  oprabid  7435  dfoprab2  7463  oprab4  7491  mpomptx  7518  elpwpwel  7759  elxp4  7916  elxp5  7917  ffoss  7942  f11o  7943  opabex3d  7962  opabex3rd  7963  opabex3  7964  abexssex  7967  elxp7  8021  dfopab2  8049  dfoprab3s  8050  fsplit  8114  frxp  8123  xporderlem  8124  frpoins3xp3g  8138  soseq  8156  suppssov1  8194  suppssov2  8195  suppssfv  8199  brtpos2  8229  tpostpos  8243  tposmpo  8260  wfrfunOLD  8331  dfrecs3  8384  dfrecs3OLD  8385  oarec  8572  oeeu  8613  eldifsucnn  8674  naddasslem1  8704  mapsncnv  8905  dfixp  8911  domen  8974  xpsnen  9067  xpcomco  9074  xpassen  9078  sbthlem9  9103  frfi  9291  marypha2lem2  9446  brttrcl2  9726  epfrs  9743  tcsni  9755  frind  9762  cp  9903  dfac5lem1  10135  dfac5lem2  10136  dfac5lem5  10139  kmlem3  10165  dfackm  10179  cfval2  10272  cflim3  10274  cfss  10277  cfslb  10278  zfcndrep  10626  eltsk2g  10763  ltexpi  10914  recmulnq  10976  ltexprlem4  11051  addsrpr  11087  mulsrpr  11088  addcnsr  11147  mulcnsr  11148  ltresr  11152  axrrecex  11175  elnnz  12596  elnn0z  12599  fnn0ind  12690  rexuz2  12913  rexrp  13028  elixx3g  13373  elfz2  13529  elfzuzb  13533  fznn  13607  elfz2nn0  13633  fznn0  13634  4fvwrd4  13663  preduz  13665  elfzo2  13677  fzind2  13799  hashgt23el  14440  hashf1lem1  14471  hashf1lem2  14472  fz1isolem  14477  s4f1o  14935  wwlktovfo  14975  fsum2dlem  15784  modfsummod  15808  prodeq1i  15930  sinltx  16205  divalglem10  16419  divalgb  16421  coprmproddvdslem  16679  isprm2  16699  infpn2  16931  prdsle  17474  prdsless  17475  prdsleval  17489  imasleval  17553  xpscf  17577  dfiso2  17783  oppcsect  17789  elhoma  18043  ispos2  18325  lubeldm  18361  glbeldm  18374  tosso  18427  ismgmhm  18672  issubmgm  18678  submgmacs  18693  ismhm  18761  issubm  18779  submacs  18803  issubg  19107  issubg3  19125  gaorb  19288  pmtrrn2  19439  efgcpbllema  19733  efgcpbllemb  19734  frgpuplem  19751  imasabl  19855  subgdmdprd  20015  dprd2d2  20025  dfrhm2  20432  opprnzrb  20479  issubrg  20529  isdomn3  20673  drngprop  20702  drngid2  20710  opprdrng  20722  isabv  20769  islss  20889  islbs  21032  lsmspsn  21040  isobs  21678  islinds  21767  isassa  21814  aspval2  21856  ltbval  21999  opsrle  22003  opsrtoslem1  22011  fvmptnn04if  22785  ntreq0  23013  restntr  23118  cnnei  23218  hausnei2  23289  cmpcov2  23326  cmpsub  23336  uncmp  23339  cmpfi  23344  llyi  23410  dissnlocfin  23465  iskgen3  23485  1stckgenlem  23489  ptpjpre1  23507  txcnpi  23544  txtube  23576  hausdiag  23581  txlm  23584  txkgen  23588  cfinfil  23829  csdfil  23830  supfil  23831  fin1aufil  23868  elflim2  23900  hauspwpwf1  23923  txflf  23942  isfcls  23945  alexsubALTlem3  23985  alexsubALT  23987  cnextcn  24003  istmd  24010  istgp  24013  tgphaus  24053  qustgplem  24057  istrg  24100  istdrg  24102  istlm  24121  blres  24368  isms2  24387  metrest  24461  metuel2  24502  restmetu  24507  isngp  24533  isnlm  24612  elii1  24880  isclmp  25046  iscvsp  25077  isncvsngp  25099  iscph  25120  cfilucfil3  25270  isbn  25288  limcrcl  25825  ig1pval3  26133  plydivex  26255  ellogdm  26598  cubic  26809  dmarea  26917  vmasum  27177  lgsquadlem1  27341  lgsquadlem2  27342  elno3  27617  slenlt  27714  madeval2  27809  elnnzs  28304  istrkg3ld  28386  legov  28510  ltgov  28522  colinearalg  28835  axeuclid  28888  axcontlem2  28890  axcontlem5  28893  nbgrel  29265  nbupgrres  29289  nbusgredgeu0  29293  nb3grprlem2  29306  nb3grpr2  29308  nb3gr2nb  29309  cplgr3v  29360  finsumvtxdg2ssteplem3  29473  wlkonprop  29584  upgrtrls  29627  upgristrl  29628  wksonproplem  29630  wksonproplemOLD  29631  usgr2pth0  29693  wwlksnext  29821  wwlksnextsurj  29828  wwlksnfi  29834  wspthsnwspthsnon  29844  wpthswwlks2on  29889  rusgrnumwwlkl1  29896  erclwwlkref  29947  isclwwlknx  29963  clwwlknwwlksn  29965  clwwlkel  29973  erclwwlknref  29996  clwlknf1oclwwlkn  30011  clwwlknonel  30022  clwwlknon1  30024  clwwlknon2x  30030  clwwlkvbij  30040  iseupthf1o  30129  2pthfrgrrn  30209  fusgr2wsp2nb  30261  numclwwlk1lem2f1  30284  numclwwlkovh  30300  numclwlk2lem2f1o  30306  frgrregord013  30322  avril1  30390  islno  30680  h2hlm  30907  hcau  31111  hhsssh2  31197  dfch2  31334  elcnop  31784  ellnop  31785  elhmop  31800  elcnfn  31809  ellnfn  31810  dmadjss  31814  adjeu  31816  adjval  31817  hhcno  31831  hhcnf  31832  eleigvec  31884  isst  32140  ishst  32141  cvnbtwn3  32215  cvnbtwn4  32216  chirredi  32321  sumdmdii  32342  an42ds  32377  an52ds  32378  an62ds  32379  an72ds  32380  an82ds  32381  or3di  32386  rexunirn  32419  rmoun  32421  dmrab  32424  difrab2  32425  iunin1f  32484  disjunsn  32521  opeldifid  32526  ofpreima  32589  mpomptxf  32601  fdifsupp  32608  1stpreima  32630  2ndpreima  32631  f1od2  32644  resf1o  32653  maprnin  32654  nndiffz1  32709  ismnt  32909  mgcval  32913  omndmul2  33026  erler  33206  isorng  33267  opprnsg  33445  1arithidom  33498  1arithufdlem4  33508  smatrcl  33773  ordtconnlem1  33901  isrrext  33977  sigaex  34087  sigaval  34088  omssubaddlem  34277  omssubadd  34278  eulerpartleme  34341  eulerpartlemt0  34347  eulerpartlemr  34352  eulerpartlemn  34359  probun  34397  ballotlemelo  34466  ballotlem2  34467  ballotlemfc0  34471  ballotlemfcc  34472  reprdifc  34605  bnj248  34677  bnj250  34678  bnj268  34686  bnj312  34689  bnj945  34750  bnj110  34835  bnj849  34902  bnj882  34903  bnj893  34905  bnj916  34910  bnj983  34928  bnj1040  34949  bnj1175  34981  cusgredgex  35090  cusgr3cyclex  35104  erdszelem1  35159  iscvm  35227  elmpst  35504  mpstrcl  35509  dfso3  35683  xpab  35689  coepr  35716  dfdm5  35736  dfrn5  35737  elima4  35739  fv1stcnv  35740  fv2ndcnv  35741  brpprod  35849  dfon3  35856  elfix  35867  dffix2  35869  elfuns  35879  brimg  35901  brapply  35902  brsuccf  35905  funpartlem  35906  funpartfun  35907  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  lineunray  36111  ellines  36116  rmoeqi  36151  reueqi  36153  itgeq12i  36170  finminlem  36282  fneval  36316  neibastop3  36326  eliminable-abelv  36833  bj-inrab  36891  bj-rest10  37052  bj-restpw  37056  bj-restuni  37061  bj-mpomptALT  37083  bj-imdirco  37154  icorempo  37315  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlpssretop  37328  pibt2  37381  wl-ifp-ncond2  37429  wl-df3-3mintru2  37450  wl-2mintru1  37454  rabiun  37563  iundif1  37564  lindsenlbs  37585  poimirlem4  37594  poimirlem25  37615  poimirlem26  37616  poimirlem29  37619  poimirlem30  37620  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  itg2addnclem2  37642  itg2addnclem3  37643  itg2addnc  37644  ftc1anc  37671  isbnd2  37753  bndss  37756  heibor1lem  37779  heibor1  37780  isrngohom  37935  isidl  37984  sbccom2lem  38094  anan  38193  eqbrb  38197  eqelb  38199  br1cnvinxp  38220  eldmqsres  38251  idinxpssinxp2  38282  moantr  38328  inxpxrn  38359  dfcoss3  38378  cocossss  38400  ressn2  38406  br1cossinidres  38413  br1cossincnvepres  38414  br1cossxrnidres  38415  br1cossxrncnvepres  38416  refrelcoss2  38428  symrelcoss2  38430  cosscnvssid5  38442  br1cossxrncnvssrres  38472  dfrefrel3  38480  dfcnvrefrel3  38495  cosselcnvrefrels2  38502  cosselcnvrefrels3  38503  cosselcnvrefrels4  38504  cosselcnvrefrels5  38505  dfsymrel3  38514  refsymrel2  38531  refsymrel3  38532  elrefsymrels3  38534  dftrrel3  38542  dfeqvrel2  38554  dfeqvrel3  38555  redundpbi1  38595  refrelredund3  38601  eldmqs1cossres  38623  dffunALTV2  38652  dffunALTV3  38653  dffunALTV4  38654  dffunALTV5  38655  dfdisjALTV  38677  dfdisjALTV2  38678  dfdisjALTV3  38679  dfdisjALTV4  38680  eldisjs3  38688  eldisjs4  38689  disjsuc  38723  prtlem70  38821  prtlem100  38823  prter2  38845  lsateln0  38959  islshpat  38981  lcvnbtwn3  38992  islfl  39024  ishlat1  39316  ishlat2  39317  cvrat4  39408  islvol5  39544  psubspset  39709  snatpsubN  39715  dalawlem13  39848  psubclsetN  39901  isltrn2N  40085  cdlemftr3  40530  dibelval3  41112  dicval2  41144  dicopelval2  41146  dicelval2N  41147  dihglb2  41307  islpolN  41448  lcfls1c  41501  mapdvalc  41594  mapdval4N  41597  mapdordlem1a  41599  aks4d1p8  42046  fimgmcyc  42504  prjsperref  42576  prjspeclsp  42582  elmzpcl  42696  mzpindd  42716  fphpd  42786  pw2f1ocnv  43008  islmodfg  43040  islssfg2  43042  dflim6  43235  onsucf1olem  43241  omge2  43269  tfsconcatlem  43307  tfsconcat0i  43316  rp-isfinite6  43489  minregex  43505  elmapintrab  43547  elinintrab  43548  relintab  43554  dfrtrcl5  43600  fsovrfovd  43980  ntrk1k3eqk13  44021  gneispace3  44104  k0004lem1  44118  pm13.192  44382  opelopab4  44524  ax6e2nd  44531  en3lplem2VD  44816  ax6e2ndVD  44880  ax6e2ndALT  44902  permaxrep  44979  iuneq1i  45057  ssrabf  45086  limcrecl  45606  dvnprodlem2  45924  fourierdlem103  46186  fourierdlem104  46187  4an21  47247  sprvalpwn0  47445  pairreueq  47472  dfvopnbgr2  47814  isubgredg  47827  xpsnopab  48080  sgrp2sgrp  48151  mpomptx2  48258  lindslinindsimp1  48381  lindslinindsimp2  48387  itsclc0b  48700  mo0sn  48742  coxp  48759  isthincd2  49271  thinccic  49305  2arwcatlem1  49420  setc1onsubc  49427  alsconv  49602  aacllem  49613