Theorem anbi1i 627

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi2ci  628  anbi12i  630  bianassc  643  anandi  676  pm5.53  1005  dfifp4  1067  dfifp5  1068  3an4anass  1107  3ioran  1108  an6  1447  an3andi  1484  an33rean  1485  an33reanOLD  1486  19.26-3an  1880  19.28v  1999  sb3an  2087  19.28  2226  eeeanv  2351  sbel2x  2473  2eu4  2655  r19.26-3  3094  r19.41v  3260  r19.41  3261  rexcomf  3270  3reeanv  3280  rabrab  3291  cbvreuw  3351  cbvreu  3356  rabeqi  3392  rabrabi  3403  ceqsex3v  3460  spc2ed  3516  rexab  3608  rexrab  3609  rmo4  3643  rmo3f  3647  reuind  3666  sbc3an  3765  rmo3  3801  ssrab  3986  rexun  4104  elin3  4114  inass  4134  rexin  4154  dfun2  4174  indifdirOLD  4200  difin2  4206  inrab2  4222  rabun2  4228  reuun2  4229  undif4  4381  rexdifpr  4574  rexsns  4585  rexdifsn  4707  2ralunsn  4806  iuncom4  4912  iindif1  4983  iunxiun  5005  disjxun  5051  zfrep4  5189  inuni  5236  reusv2lem4  5294  reusv2  5296  otth2  5367  copsexgw  5373  copsexg  5374  copsex2g  5376  copsex4g  5378  vopelopabsb  5410  rabxp  5597  opeliunxp  5616  xpundir  5618  xpiundi  5619  xpiundir  5620  brinxp2  5626  copsex2gb  5676  dminss  6016  imainss  6017  difxp  6027  cnvresima  6093  coundi  6111  resco  6114  imaco  6115  rnco  6116  coiun  6120  coi1  6126  coass  6129  cnvpo  6150  xpco  6152  frpoind  6196  wfi  6203  dffun2  6390  fncnv  6453  imadif  6464  mptun  6524  ffrnb  6560  dff1o2  6666  dff1o3  6667  brprcneu  6708  fvprc  6709  fvun2  6803  eqfnfv3  6854  respreima  6886  f1ompt  6928  f1ossf1o  6943  fsn  6950  fmptsng  6983  fmptsnd  6984  tpres  7016  abrexco  7057  imaiun  7058  f1mpt  7073  dff1o6  7086  oprabidw  7244  oprabid  7245  dfoprab2  7269  oprab4  7297  mpomptx  7323  elpwpwel  7552  elxp4  7700  elxp5  7701  ffoss  7719  f11o  7720  opabex3d  7738  opabex3rd  7739  opabex3  7740  abexssex  7743  elxp7  7796  dfopab2  7822  dfoprab3s  7823  fsplit  7885  frxp  7893  xporderlem  7894  suppssov1  7940  suppssfv  7944  brtpos2  7974  tpostpos  7988  tposmpo  8005  wfrfun  8065  dfrecs3  8109  oarec  8290  oeeu  8331  mapsncnv  8574  dfixp  8580  domen  8641  xpsnen  8729  xpcomco  8735  xpassen  8739  sbthlem9  8764  frfi  8916  marypha2lem2  9052  epfrs  9347  tcsni  9359  frind  9366  cp  9507  dfac5lem1  9737  dfac5lem2  9738  dfac5lem5  9741  kmlem3  9766  dfackm  9780  cfval2  9874  cflim3  9876  cfss  9879  cfslb  9880  zfcndrep  10228  eltsk2g  10365  ltexpi  10516  recmulnq  10578  ltexprlem4  10653  addsrpr  10689  mulsrpr  10690  addcnsr  10749  mulcnsr  10750  ltresr  10754  axrrecex  10777  elnnz  12186  elnn0z  12189  fnn0ind  12276  rexuz2  12495  rexrp  12607  elixx3g  12948  elfz2  13102  elfzuzb  13106  fznn  13180  elfz2nn0  13203  fznn0  13204  4fvwrd4  13232  preduz  13234  elfzo2  13246  fzind2  13360  hashgt23el  13991  hashf1lem1  14020  hashf1lem1OLD  14021  hashf1lem2  14022  fz1isolem  14027  s4f1o  14483  wwlktovfo  14525  fsum2dlem  15334  modfsummod  15358  sinltx  15750  divalglem10  15963  divalgb  15965  coprmproddvdslem  16219  isprm2  16239  infpn2  16466  prdsle  16967  prdsless  16968  prdsleval  16982  imasleval  17046  xpscf  17070  dfiso2  17277  oppcsect  17283  elhoma  17538  ispos2  17822  lubeldm  17859  glbeldm  17872  tosso  17925  ismhm  18220  issubm  18230  submacs  18253  issubg  18543  issubg3  18561  gaorb  18701  pmtrrn2  18852  efgcpbllema  19144  efgcpbllemb  19145  frgpuplem  19162  subgdmdprd  19421  dprd2d2  19431  dfrhm2  19737  drngprop  19778  drngid2  19783  opprdrng  19791  issubrg  19800  isabv  19855  islss  19971  islbs  20113  lsmspsn  20121  isobs  20682  islinds  20771  isassa  20818  aspval2  20858  ltbval  21000  opsrle  21004  opsrtoslem1  21012  fvmptnn04if  21746  ntreq0  21974  restntr  22079  cnnei  22179  hausnei2  22250  cmpcov2  22287  cmpsub  22297  uncmp  22300  cmpfi  22305  llyi  22371  dissnlocfin  22426  iskgen3  22446  1stckgenlem  22450  ptpjpre1  22468  txcnpi  22505  txtube  22537  hausdiag  22542  txlm  22545  txkgen  22549  cfinfil  22790  csdfil  22791  supfil  22792  fin1aufil  22829  elflim2  22861  hauspwpwf1  22884  txflf  22903  isfcls  22906  alexsubALTlem3  22946  alexsubALT  22948  cnextcn  22964  istmd  22971  istgp  22974  tgphaus  23014  qustgplem  23018  istrg  23061  istdrg  23063  istlm  23082  blres  23329  isms2  23348  metrest  23422  metuel2  23463  restmetu  23468  isngp  23494  isnlm  23573  elii1  23832  isclmp  23994  iscvsp  24025  isncvsngp  24046  iscph  24067  cfilucfil3  24217  isbn  24235  limcrcl  24771  ig1pval3  25072  plydivex  25190  ellogdm  25527  cubic  25732  dmarea  25840  vmasum  26097  lgsquadlem1  26261  lgsquadlem2  26262  istrkg3ld  26552  legov  26676  ltgov  26688  colinearalg  27001  axeuclid  27054  axcontlem2  27056  axcontlem5  27059  nbgrel  27428  nbupgrres  27452  nbusgredgeu0  27456  nb3grprlem2  27469  nb3grpr2  27471  nb3gr2nb  27472  cplgr3v  27523  finsumvtxdg2ssteplem3  27635  wlkonprop  27746  upgrtrls  27789  upgristrl  27790  wksonproplem  27792  usgr2pth0  27852  wwlksnext  27977  wwlksnextsurj  27984  wwlksnfi  27990  wspthsnwspthsnon  28000  wpthswwlks2on  28045  rusgrnumwwlkl1  28052  erclwwlkref  28103  isclwwlknx  28119  clwwlknwwlksn  28121  clwwlkel  28129  erclwwlknref  28152  clwlknf1oclwwlkn  28167  clwwlknonel  28178  clwwlknon1  28180  clwwlknon2x  28186  clwwlkvbij  28196  iseupthf1o  28285  2pthfrgrrn  28365  fusgr2wsp2nb  28417  numclwwlk1lem2f1  28440  numclwwlkovh  28456  numclwlk2lem2f1o  28462  frgrregord013  28478  avril1  28546  islno  28834  h2hlm  29061  hcau  29265  hhsssh2  29351  dfch2  29488  elcnop  29938  ellnop  29939  elhmop  29954  elcnfn  29963  ellnfn  29964  dmadjss  29968  adjeu  29970  adjval  29971  hhcno  29985  hhcnf  29986  eleigvec  30038  isst  30294  ishst  30295  cvnbtwn3  30369  cvnbtwn4  30370  chirredi  30475  sumdmdii  30496  or3di  30529  rexunirn  30559  rmoun  30561  dmrab  30563  difrab2  30564  iunin1f  30616  disjunsn  30652  opeldifid  30657  ofpreima  30722  mpomptxf  30736  1stpreima  30759  2ndpreima  30760  f1od2  30776  resf1o  30785  maprnin  30786  nndiffz1  30827  ismnt  30980  mgcval  30984  omndmul2  31057  isorng  31217  smatrcl  31460  ordtconnlem1  31588  isrrext  31662  sigaex  31790  sigaval  31791  omssubaddlem  31978  omssubadd  31979  eulerpartleme  32042  eulerpartlemt0  32048  eulerpartlemr  32053  eulerpartlemn  32060  probun  32098  ballotlemelo  32166  ballotlem2  32167  ballotlemfc0  32171  ballotlemfcc  32172  reprdifc  32319  bnj248  32391  bnj250  32392  bnj268  32400  bnj312  32403  bnj945  32466  bnj110  32551  bnj849  32618  bnj882  32619  bnj893  32621  bnj916  32626  bnj983  32644  bnj1040  32665  bnj1175  32697  cusgredgex  32796  cusgr3cyclex  32811  erdszelem1  32866  iscvm  32934  elmpst  33211  mpstrcl  33216  dfso3  33379  riotarab  33388  reurab  33389  xpab  33392  ot2elxp  33395  imaeqsexv  33406  eldifsucnn  33410  coepr  33438  dfpo2  33441  dfdm5  33466  dfrn5  33467  elima4  33469  fv1stcnv  33470  fv2ndcnv  33471  brttrcl2  33513  soseq  33540  elno3  33595  slenlt  33692  madeval2  33774  brpprod  33924  dfon3  33931  elfix  33942  dffix2  33944  elfuns  33954  brimg  33976  brapply  33977  brsuccf  33980  funpartlem  33981  funpartfun  33982  brrestrict  33988  dfrecs2  33989  dfrdg4  33990  lineunray  34186  ellines  34191  finminlem  34244  fneval  34278  neibastop3  34288  eliminable-abelv  34790  bj-inrab  34852  bj-rest10  34994  bj-restpw  34998  bj-restuni  35003  bj-mpomptALT  35025  bj-imdirco  35096  icorempo  35259  isbasisrelowllem1  35263  isbasisrelowllem2  35264  relowlpssretop  35272  pibt2  35325  wl-ifp-ncond2  35373  wl-df3-3mintru2  35394  wl-2mintru1  35398  rabiun  35487  iundif1  35488  lindsenlbs  35509  poimirlem4  35518  poimirlem25  35539  poimirlem26  35540  poimirlem29  35543  poimirlem30  35544  ismblfin  35555  ovoliunnfl  35556  voliunnfl  35558  volsupnfl  35559  itg2addnclem2  35566  itg2addnclem3  35567  itg2addnc  35568  ftc1anc  35595  isbnd2  35678  bndss  35681  heibor1lem  35704  heibor1  35705  isrngohom  35860  isidl  35909  sbccom2lem  36019  anan  36116  eqelb  36119  eldmqsres  36158  idinxpssinxp2  36190  moantr  36231  inxpxrn  36258  dfcoss3  36277  cocossss  36296  br1cossinidres  36304  br1cossincnvepres  36305  br1cossxrnidres  36306  br1cossxrncnvepres  36307  refrelcoss2  36319  symrelcoss2  36321  cosscnvssid5  36333  br1cossxrncnvssrres  36363  dfrefrel3  36371  dfcnvrefrel3  36384  cosselcnvrefrels2  36389  cosselcnvrefrels3  36390  cosselcnvrefrels4  36391  cosselcnvrefrels5  36392  dfsymrel3  36401  refsymrel2  36418  refsymrel3  36419  elrefsymrels3  36421  dftrrel3  36429  dfeqvrel2  36440  dfeqvrel3  36441  redundpbi1  36481  refrelredund3  36487  eldmqs1cossres  36508  dffunALTV2  36536  dffunALTV3  36537  dffunALTV4  36538  dffunALTV5  36539  dfdisjALTV  36561  dfdisjALTV2  36562  dfdisjALTV3  36563  dfdisjALTV4  36564  eldisjs3  36572  eldisjs4  36573  prtlem70  36608  prtlem100  36610  prter2  36632  lsateln0  36746  islshpat  36768  lcvnbtwn3  36779  islfl  36811  ishlat1  37103  ishlat2  37104  cvrat4  37194  islvol5  37330  psubspset  37495  snatpsubN  37501  dalawlem13  37634  psubclsetN  37687  isltrn2N  37871  cdlemftr3  38316  dibelval3  38898  dicval2  38930  dicopelval2  38932  dicelval2N  38933  dihglb2  39093  islpolN  39234  lcfls1c  39287  mapdvalc  39380  mapdval4N  39383  mapdordlem1a  39385  prjsperref  40153  prjspeclsp  40159  elmzpcl  40251  mzpindd  40271  fphpd  40341  pw2f1ocnv  40562  islmodfg  40597  islssfg2  40599  isdomn3  40732  rp-isfinite6  40810  elmapintrab  40860  elinintrab  40861  relintab  40867  dfrtrcl5  40913  fsovrfovd  41294  ntrk1k3eqk13  41337  gneispace3  41420  k0004lem1  41434  pm13.192  41701  opelopab4  41844  ax6e2nd  41851  en3lplem2VD  42137  ax6e2ndVD  42201  ax6e2ndALT  42223  ssrabf  42337  limcrecl  42845  dvnprodlem2  43163  fourierdlem103  43425  fourierdlem104  43426  4an21  44434  sprvalpwn0  44608  pairreueq  44635  xpsnopab  44992  ismgmhm  45010  issubmgm  45016  submgmacs  45031  sgrp2sgrp  45095  opeliun2xp  45341  mpomptx2  45343  lindslinindsimp1  45471  lindslinindsimp2  45477  itsclc0b  45791  mo0sn  45834  iscnrm3lem3  45902  isthincd2  45992  thinccic  46015  alsconv  46165  aacllem  46176