Theorem anbi1i 636

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi2ci  637  bianbi  639  anandi  689  3an4anass  1122  3ioran  1123  4anpull2OLD  1383  an33rean  1514  an42ds  1520  19.26-3an  1905  sb3an  2118  eeeanv  2379  sbel2x  2503  rexcomf  3301  cbvreu  3404  rabeqi  3425  rabrabi  3430  rabrab  3435  ceqsex3v  3502  spc2ed  3555  rexrab  3654  reurab  3659  rmo3f  3692  reuind  3711  rmo3  3836  ssrab  4019  rexun  4142  elin3  4152  inass  4173  rexin  4196  dfun2  4216  inrab2  4263  rabun2  4270  reuun2  4271  undif4  4420  rexdifpr  4620  rexsns  4632  rexdifsn  4757  2ralunsn  4855  iuncom4  4960  iindif1  5035  iunxiun  5057  disjxun  5101  zfrep4  5248  inuni  5314  reusv2lem4  5366  reusv2  5368  otth2  5459  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  copsex2g  5470  copsex4g  5472  vopelopabsb  5507  rabxp  5703  opeliunxp  5722  opeliun2xp  5723  xpundir  5725  xpiundi  5726  xpiundir  5727  brinxp2  5733  copsex2gb  5787  cnvopab  6131  dminss  6144  imainss  6145  difxp  6156  cnvresima  6226  coundi  6243  resco  6246  imaco  6247  rnco  6248  rncoOLD  6249  coiun  6253  coi1  6259  coass  6262  cnvpo  6285  xpco  6287  dfpo2  6294  frpoind  6340  dffun2  6543  fncnv  6607  imadif  6618  mptun  6679  ffrnb  6718  dff1o2  6824  dff1o3  6825  brprcneu  6869  brprcneuALT  6870  fvun2  6971  eqfnfv3  7025  respreima  7059  f1ompt  7105  f1ossf1o  7123  fsn  7130  fmptsng  7167  fmptsnd  7168  tpres  7201  abrexco  7242  imaiun  7243  f1mpt  7259  dff1o6  7277  riotarab  7413  oprabidw  7445  oprabid  7446  dfoprab2  7472  oprab4  7500  mpomptx  7527  elpwpwel  7767  elxp4  7920  elxp5  7921  ffoss  7944  f11o  7945  opabex3d  7963  opabex3rd  7964  opabex3  7965  abexssex  7968  elxp7  8022  dfopab2  8050  dfoprab3s  8051  fsplit  8115  frxp  8125  xporderlem  8126  frpoins3xp3g  8140  soseq  8158  suppssov1  8196  suppssov2  8197  suppssfv  8201  brtpos2  8231  tpostpos  8245  tposmpo  8262  dfrecs3  8362  oarec  8550  oeeu  8592  eldifsucnn  8653  naddasslem1  8684  mapsncnv  8901  dfixp  8907  domen  8968  xpsnen  9060  xpcomco  9066  xpassen  9070  sbthlem9  9094  frfi  9256  marypha2lem2  9407  brttrcl2  9694  epfrs  9711  tcsni  9721  frind  9733  cp  9894  dfac5lem1  10127  dfac5lem2  10128  dfac5lem5  10131  kmlem3  10156  dfackm  10170  cfval2  10263  cflim3  10265  cfss  10268  cfslb  10269  zfcndrep  10624  eltsk2g  10761  ltexpi  10912  recmulnq  10974  ltexprlem4  11049  addsrpr  11085  mulsrpr  11086  addcnsr  11145  mulcnsr  11146  ltresr  11150  axrrecex  11173  elnnz  12626  elnn0z  12629  fnn0ind  12721  rexuz2  12949  rexrp  13066  elixx3g  13412  elfz2  13569  elfzuzb  13573  fznn  13648  elfz2nn0  13674  fznn0  13675  4fvwrd4  13704  preduz  13706  elfzo2  13718  fzind2  13845  hashgt23el  14490  hashf1lem1  14521  hashf1lem2  14522  fz1isolem  14527  s4f1o  14990  wwlktovfo  15032  fsum2dlem  15857  modfsummod  15882  prodeq1i  16006  sinltx  16278  divalglem10  16493  divalgb  16495  coprmproddvdslem  16753  isprm2  16773  infpn2  17006  prdsle  17548  prdsless  17549  prdsleval  17563  imasleval  17628  xpscf  17652  dfiso2  17862  oppcsect  17868  elhoma  18122  ispos2  18404  lubeldm  18440  glbeldm  18453  tosso  18506  ismgmhm  18799  issubmgm  18805  submgmacs  18820  ismhm  18894  issubm  18912  submacs  18937  issubg  19250  issubg3  19269  gaorb  19435  pmtrrn2  19588  efgcpbllema  19882  efgcpbllemb  19883  frgpuplem  19900  imasabl  20004  subgdmdprd  20164  dprd2d2  20174  omndmul2  20261  dfrhm2  20616  isrhm0  20618  opprnzrb  20683  issubrg  20734  isdomn3  20877  drngprop  20908  drngid2  20920  opprdrng  20931  isabv  20978  isorng  21028  islss  21119  islbs  21261  lsmspsn  21269  isobs  21934  islinds  22023  lindsenlbs  22065  isassa  22072  aspval2  22114  ltbval  22260  opsrle  22264  opsrtoslem1  22272  fvmptnn04if  23075  ntreq0  23303  restntr  23408  cnnei  23508  hausnei2  23579  cmpcov2  23616  cmpsub  23626  uncmp  23629  cmpfi  23634  llyi  23701  dissnlocfin  23756  iskgen3  23776  1stckgenlem  23780  ptpjpre1  23798  txcnpi  23835  txtube  23867  hausdiag  23872  txlm  23875  txkgen  23879  cfinfil  24120  csdfil  24121  supfil  24122  fin1aufil  24159  elflim2  24191  hauspwpwf1  24214  txflf  24233  isfcls  24236  alexsubALTlem3  24276  alexsubALT  24278  cnextcn  24294  istmd  24301  istgp  24304  tgphaus  24344  qustgplem  24348  istrg  24391  istdrg  24393  istlm  24412  blres  24658  isms2  24677  metrest  24751  metuel2  24792  restmetu  24797  isngp  24823  isnlm  24902  elii1  25164  isclmp  25326  iscvsp  25357  isncvsngp  25378  iscph  25399  cfilucfil3  25549  isbn  25567  limcrcl  26102  ig1pval3  26404  plydivex  26528  ellogdm  26877  cubic  27087  dmarea  27195  vmasum  27453  lgsquadlem1  27617  lgsquadlem2  27618  elno3  27892  lenlts  27989  madeval2  28099  elnnzs  28667  istrkg3ld  28803  legov  28928  ltgov  28940  colinearalg  29368  axeuclid  29421  axcontlem2  29423  axcontlem5  29426  nbgrel  29801  nbupgrres  29825  nbusgredgeu0  29829  nb3grprlem2  29842  nb3grpr2  29844  nb3gr2nb  29845  cplgr3v  29896  finsumvtxdg2ssteplem3  30008  wlkonprop  30117  upgrtrls  30164  upgristrl  30165  wksonproplem  30167  usgr2pth0  30231  wwlksnext  30362  wwlksnextsurj  30369  wwlksnfi  30375  wspthsnwspthsnon  30385  wpthswwlks2on  30433  rusgrnumwwlkl1  30440  erclwwlkref  30491  isclwwlknx  30507  clwwlknwwlksn  30509  clwwlkel  30517  erclwwlknref  30540  clwlknf1oclwwlkn  30555  clwwlknonel  30566  clwwlknon1  30568  clwwlknon2x  30574  clwwlkvbij  30584  iseupthf1o  30683  2pthfrgrrn  30763  fusgr2wsp2nb  30815  numclwwlk1lem2f1  30838  numclwwlkovh  30854  numclwlk2lem2f1o  30860  frgrregord013  30876  avril1  30944  islno  31235  h2hlm  31462  hcau  31666  hhsssh2  31752  dfch2  31889  elcnop  32339  ellnop  32340  elhmop  32355  elcnfn  32364  ellnfn  32365  dmadjss  32369  adjeu  32371  adjval  32372  hhcno  32386  hhcnf  32387  eleigvec  32439  isst  32695  ishst  32696  cvnbtwn3  32770  cvnbtwn4  32771  chirredi  32876  sumdmdii  32897  an52ds  32932  an62ds  32933  an72ds  32934  an82ds  32935  or3di  32937  rexunirn  32968  rmoun  32970  dmrab  32973  difrab2  32974  iunin1f  33032  disjunsn  33068  opeldifid  33073  ofpreima  33139  mpomptxf  33152  fdifsupp  33158  1stpreima  33180  2ndpreima  33181  f1od2  33191  resf1o  33202  maprnin  33203  nndiffz1  33258  ismnt  33424  mgcval  33428  erler  33706  opprnsg  33887  1arithidom  33948  1arithufdlem4  33958  extdgfialglem1  34203  smatrcl  34307  ordtconnlem1  34435  isrrext  34511  sigaex  34621  sigaval  34622  omssubaddlem  34811  omssubadd  34812  eulerpartleme  34875  eulerpartlemt0  34881  eulerpartlemr  34886  eulerpartlemn  34893  probun  34931  ballotlemelo  35000  ballotlem2  35001  ballotlemfc0  35005  ballotlemfcc  35006  reprdifc  35136  bnj248  35211  bnj250  35212  bnj268  35220  bnj312  35223  bnj945  35284  bnj110  35368  bnj849  35435  bnj882  35436  bnj893  35438  bnj916  35443  bnj983  35461  bnj1040  35482  bnj1175  35514  cusgredgex  35721  cusgr3cyclex  35726  erdszelem1  35771  iscvm  35839  elmpst  36116  mpstrcl  36121  dfso3  36300  xpab  36306  coepr  36333  dfdm5  36353  dfrn5  36354  elima4  36356  fv1stcnv  36357  fv2ndcnv  36358  brpprod  36463  dfon3  36470  elfix  36481  dffix2  36483  elfuns  36493  brimg  36515  brapply  36516  lemsuccf  36519  funpartlem  36522  funpartfun  36523  brrestrict  36529  dfrecs2  36530  dfrdg4  36531  lineunray  36728  ellines  36733  rmoeqi  36808  reueqi  36810  itgeq12i  36827  finminlem  36938  fneval  36972  neibastop3  36982  eliminable-abelv  37613  bj-inrab  37672  bj-axseprep  37820  bj-rest10  37839  bj-restpw  37843  bj-restuni  37848  bj-mpomptALT  37870  copsex2gd  37891  bj-imdirco  37943  icorempo  38106  isbasisrelowllem1  38110  isbasisrelowllem2  38111  relowlpssretop  38119  pibt2  38172  wl-ifp-ncond2  38220  wl-df3-3mintru2  38241  wl-2mintru1  38245  rabiun  38353  iundif1  38354  poimirlem4  38374  poimirlem25  38395  poimirlem26  38396  poimirlem29  38399  poimirlem30  38400  ismblfin  38411  ovoliunnfl  38412  voliunnfl  38414  volsupnfl  38415  itg2addnclem2  38422  itg2addnclem3  38423  itg2addnc  38424  ftc1anc  38451  isbnd2  38534  bndss  38537  heibor1lem  38560  heibor1  38561  isrngohom  38716  isidl  38765  sbccom2lem  38873  anan  38984  eqbrb  38988  eqelb  38990  br1cnvinxp  39008  eldmqsres  39042  idinxpssinxp2  39073  moantr  39121  inxpxrn  39167  blockadjliftmap  39207  dfcoss3  39253  cocossss  39275  ressn2  39281  br1cossinidres  39288  br1cossincnvepres  39289  br1cossxrnidres  39290  br1cossxrncnvepres  39291  refrelcoss2  39303  symrelcoss2  39305  cosscnvssid5  39317  br1cossxrncnvssrres  39337  dfrefrel3  39345  dfcnvrefrel3  39360  cosselcnvrefrels2  39367  cosselcnvrefrels3  39368  cosselcnvrefrels4  39369  cosselcnvrefrels5  39370  dfsymrel3  39383  refsymrel2  39400  refsymrel3  39401  elrefsymrels3  39403  dftrrel3  39411  dfeqvrel2  39423  dfeqvrel3  39424  redundpbi1  39464  refrelredund3  39470  eldmqs1cossres  39493  dffunALTV2  39522  dffunALTV3  39523  dffunALTV4  39524  dffunALTV5  39525  dfdisjALTV  39547  dfdisjALTV2  39548  dfdisjALTV3  39549  dfdisjALTV4  39550  disjimdmqseq  39558  eldisjs3  39570  eldisjs4  39571  disjsuc  39608  prtlem70  39731  prtlem100  39733  prter2  39755  lsateln0  39869  islshpat  39891  lcvnbtwn3  39902  islfl  39934  ishlat1  40226  ishlat2  40227  cvrat4  40317  islvol5  40453  psubspset  40618  snatpsubN  40624  dalawlem13  40757  psubclsetN  40810  isltrn2N  40994  cdlemftr3  41439  dibelval3  42021  dicval2  42053  dicopelval2  42055  dicelval2N  42056  dihglb2  42216  islpolN  42357  lcfls1c  42410  mapdvalc  42503  mapdval4N  42506  mapdordlem1a  42508  aks4d1p8  42954  fimgmcyc  43417  prjsperref  43453  prjspeclsp  43459  elmzpcl  43572  mzpindd  43592  fphpd  43658  pw2f1ocnv  43879  islmodfg  43911  islssfg2  43913  dflim6  44106  onsucf1olem  44112  omge2  44140  tfsconcatlem  44178  tfsconcat0i  44187  rp-isfinite6  44359  minregex  44375  elmapintrab  44417  elinintrab  44418  relintab  44424  dfrtrcl5  44470  fsovrfovd  44850  ntrk1k3eqk13  44891  gneispace3  44974  k0004lem1  44988  pm13.192  45235  opelopab4  45375  ax6e2nd  45382  en3lplem2VD  45667  ax6e2ndVD  45731  ax6e2ndALT  45753  permaxrep  45830  iuneq1i  45919  ssrabf  45947  limcrecl  46460  dvnprodlem2  46776  fourierdlem103  47038  fourierdlem104  47039  4an21  48159  sprvalpwn0  48384  pairreueq  48411  dfvopnbgr2  48770  isubgredg  48783  xpsnopab  49074  sgrp2sgrp  49144  mpomptx2  49266  lindslinindsimp1  49388  lindslinindsimp2  49394  itsclc0b  49703  mo0sn  49745  coxp  49762  isthincd2  50364  thinccic  50398  2arwcatlem1  50522  setc1onsubc  50529  alsanmo  50740  ralsanmo  50741  alsralrex  50742  aacllem  50773