Theorem anbi2i 624

Description: Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
anbi2i	⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32i 577	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anbi1ci  627  anbi12i  628  bianass  640  an42  655  anandir  675  dfbi3  1044  dn1  1052  dfifp3  1060  an3andi  1478  an33rean  1479  an33reanOLD  1480  anxordi  1518  norassOLD  1534  cadcoma  1613  nic-mpALT  1673  nic-axALT  1675  3exdistr  1962  4exdistr  1963  19.27v  1996  19.27  2229  19.41  2237  2sb5  2282  dfsb7  2285  dfsb7OLD  2286  sbnOLD  2541  sbnALT  2595  dfeumo  2619  mo4f  2651  eu3v  2655  eu6  2659  dfeu  2681  eu2  2693  eu4  2699  2mos  2734  2eu4  2739  rexbii  3247  ceqsex3v  3545  ceqsex4v  3546  ceqsex8v  3548  reu2  3716  reu6  3717  reu4  3722  reu7  3723  rmo3f  3725  rmo4f  3726  2reu5lem3  3748  2reu5  3749  rmo3  3872  rmo3OLD  3873  reuan  3880  dfpss2  4062  difdif  4107  raldifb  4121  inass  4196  dfss4  4235  dfin2  4237  indi  4250  indifdir  4260  undif3  4265  difin0ss  4328  inssdif0  4329  2nreu  4393  2reu4lem  4465  rexdifpr  4598  reuprg0  4638  ssdifsn  4720  ssunpr  4765  unipr  4855  uniun  4861  uniin  4862  csbuni  4867  iunin2  4993  iundif2  4996  iindif2  4999  iinin2  5000  elpwpw  5024  axrep1  5191  axrep4  5195  notzfausOLD  5263  reusv2lem4  5302  eqvinop  5378  opcom  5391  fconstmpt  5614  opeliunxp  5619  xpundi  5620  elvvv  5627  opelinxp  5631  xpiindi  5706  elcnv2  5748  cnvuni  5757  dmuni  5783  brres  5860  dmres  5875  elidinxp  5911  restidsing  5922  elima3  5936  asymref  5976  imainss  6011  difxp  6021  xpdifid  6025  mptpreima  6092  coundir  6101  resco  6103  coass  6118  relrelss  6124  opreu2reurex  6145  wfi  6181  ordtri3or  6223  dffun2  6365  dffun3  6366  dffun4  6367  dffun5  6368  dffun6f  6369  dffun7  6382  dffun8  6383  dffun9  6384  svrelfun  6426  fncnv  6427  imadif  6438  dfmpt3  6482  fcnvres  6556  fint  6558  fin  6559  dff12  6574  fores  6600  dff1o4  6623  eqfnfv3  6804  fndmin  6815  fniniseg  6830  unpreima  6833  ffnfvf  6883  fsn2  6898  tpres  6963  fconstfv  6975  dff13f  7014  dff14a  7028  dff14b  7029  isocnv2  7084  f1opr  7210  ffnov  7278  eqfnov  7280  foov  7322  uniuni  7484  tfindsg  7575  findsg  7609  funcnvuni  7636  opabex3d  7666  opabex3rd  7667  opabex3  7668  1stconst  7795  2ndconst  7796  frxp  7820  soxp  7823  suppvalbr  7834  suppofssd  7867  mpoxopovel  7886  brtpos  7901  tpostpos  7912  dfsmo2  7984  dfrecs3  8009  rdglem1  8051  tz7.49  8081  brwitnlem  8132  oeeu  8229  erinxp  8371  mapsncnv  8457  cbvixp  8478  ixpin  8487  ixpiin  8488  mptelixpg  8499  elixpsn  8501  ixpsnf1o  8502  xpassen  8611  omxpenlem  8618  sbthcl  8639  wemapsolem  9014  dford2  9083  inf2  9086  zfinf  9102  trcl  9170  iscard2  9405  leweon  9437  aceq1  9543  dfac3  9547  dfac4  9548  dfac5lem2  9550  dfac5  9554  kmlem3  9578  kmlem4  9579  kmlem14  9589  kmlem15  9590  dfackm  9592  infmap2  9640  fin23lem25  9746  zorn2lem7  9924  brdom6disj  9954  zfcndrep  10036  zfcndinf  10040  fpwwe  10068  axgroth4  10254  grothprim  10256  grothtsk  10257  nqpr  10436  addsrmo  10495  mulsrmo  10496  opelreal  10552  elnnz  11992  elznn0nn  11996  peano2uz2  12071  nnwos  12316  dflt2  12542  xmullem  12658  4fvwrd4  13028  preduz  13030  elfznelfzo  13143  fzind2  13156  fsuppmapnn0fiubex  13361  hashinfxadd  13747  hashgt23el  13786  hashfun  13799  fi1uzind  13856  brfi1uzind  13857  opfi1uzind  13860  cotr2g  14336  shftdm  14430  rexfiuz  14707  cbvsum  15052  mertenslem2  15241  mertens  15242  cbvprod  15269  prodmo  15290  iprodmul  15357  divalglem10  15753  ndvdssub  15760  bitsmod  15785  algcvgblem  15921  isprm2  16026  isprm4  16028  hashdvds  16112  infpn2  16249  hashbc0  16341  xpscf  16838  funcpropd  17170  isffth2  17186  eldmcoa  17325  setcinv  17350  xpccatid  17438  yonedainv  17531  ispos  17557  ispos2  17558  joinfval2  17612  meetfval2  17626  istsr2  17828  isnsg2  18308  isnsg4  18319  isgim  18402  oppgid  18484  oppgcntz  18492  symgfix2  18544  efgval2  18850  iscyg2  19001  dmdprdd  19121  subgdmdprd  19156  issrg  19257  oppr1  19384  opprunit  19411  opprirred  19452  isrhm  19473  subsubrg2  19562  islmim  19834  lbsextg  19934  lidlnz  20001  isdomn2  20072  opsrtoslem1  20264  resubdrg  20752  unocv  20824  pjfval2  20853  islinds2  20957  mdetunilem8  21228  istop2g  21504  isbasis2g  21556  tgval2  21564  isclo2  21696  isnrm2  21966  is1stc2  22050  llyi  22082  isfbas2  22443  elfg  22479  ufinffr  22537  isfcls  22617  alexsubALTlem2  22656  alexsubALTlem3  22657  cnextcn  22675  ustfilxp  22821  iscusp2  22911  metustid  23164  isclmp  23701  iscvsp  23732  tcphcph  23840  iscau3  23881  caucfil  23886  ellogdm  25222  dvdsflsumcom  25765  logfac2  25793  dchrelbas3  25814  dchrvmasumlema  26076  legtrid  26377  outpasch  26541  axcontlem5  26754  axcontlem6  26755  axcontlem7  26756  nb3grpr2  27165  iscplgr  27197  pthdlem1  27547  wwlksnextinj  27677  usgr2wspthon  27744  rusgrnumwwlkl1  27747  isclwwlk  27762  clwwlkccatlem  27767  clwwlknon2x  27882  iseupthf1o  27981  frcond3  28048  frgr3v  28054  4cycl2vnunb  28069  frgrncvvdeqlem2  28079  fusgr2wsp2nb  28113  numclwlk1lem1  28148  hhcms  28980  isch3  29018  ocsh  29060  pjhtheu  29171  pjpreeq  29175  h1deoi  29326  h1dei  29327  eleigvec  29734  cvbr2  30060  cvnbtwn2  30064  cvnbtwn4  30066  mdsl2i  30099  cvmdi  30101  mdsymlem6  30185  cdj3lem3b  30217  mo5f  30253  nmo  30254  rexunirn  30256  dmrab  30260  difrab2  30261  disjunsn  30344  unipreima  30391  dfcnv2  30422  1stpreima  30442  ssmxidl  30979  isrnsiga  31372  rossros  31439  omsmeas  31581  eulerpartlemr  31632  eulerpartlemgvv  31634  ballotlemodife  31755  plymulx  31818  signstfvneq0  31842  bnj251  31972  bnj252  31973  bnj257  31977  bnj290  31980  bnj1304  32091  bnj153  32152  bnj543  32165  bnj571  32178  bnj580  32185  bnj607  32188  bnj882  32198  bnj964  32215  bnj996  32228  bnj1033  32241  bnj1176  32277  bnj1186  32279  bnj1189  32281  bnj1204  32284  bnj1253  32289  bnj1452  32324  bnj1463  32327  dff15  32353  lfuhgr3  32366  cusgredgex2  32369  usgrgt2cycl  32377  2cycl2d  32386  dfacycgr1  32391  erdszelem9  32446  cvmlift2lem9  32558  cvmlift2lem13  32562  satfvsucsuc  32612  satfdm  32616  satf0  32619  fmlasucdisj  32646  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  elmthm  32823  axinfprim  32932  axacprim  32933  dfso2  32990  dfpo2  32991  dford5reg  33027  dfon2lem5  33032  dfon2  33037  trpredmintr  33070  frpoind  33080  frind  33085  frr3g  33121  nosupno  33203  dmscut  33272  brtxp2  33342  brpprod3a  33347  dfom5b  33373  brcart  33393  brimg  33398  funpartlem  33403  dfrecs2  33411  cgrxfr  33516  segletr  33575  trer  33664  fneval  33700  neifg  33719  df3nandALT1  33747  andnand1  33749  nandsym1  33770  bj-eu3f  34165  bj-csbsnlem  34223  bj-snsetex  34278  bj-elsngl  34283  bj-snglc  34284  bj-restuni  34391  bj-dfmpoa  34413  bj-isrvec  34578  mptsnunlem  34622  icorempo  34635  isbasisrelowllem2  34640  relowlpssretop  34648  rdgeqoa  34654  difunieq  34658  dffinxpf  34669  nlpineqsn  34692  wl-ifpdfbi  34749  wl-dfrabsb  34876  curf  34885  finixpnum  34892  ptrest  34906  poimirlem1  34908  poimirlem14  34921  poimirlem16  34923  poimirlem19  34926  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimir  34940  cnambfre  34955  itg2addnc  34961  ftc1anc  34990  opropabco  35014  isdrngo1  35249  keridl  35325  ispridlc  35363  selconj  35393  eldmqsres  35558  cnvepres  35570  ecinn0  35622  alrmomorn  35627  moantr  35631  dfxrn2  35643  inxpxrn  35658  rnxrnres  35662  refrelredund4  35885  dferALTV2  35917  dfeldisj3  35967  prtlem70  36008  prtlem100  36010  prtlem15  36026  islshpat  36168  lcvbr2  36173  lcvbr3  36174  lcvnbtwn2  36178  ellkr  36240  cvrval2  36425  cvrnbtwn2  36426  cvrnbtwn3  36427  cvrnbtwn4  36430  ishlat2  36504  lplnexatN  36714  islvol5  36730  dath  36887  pclfinclN  37101  lhpexle3  37163  4atex2  37228  4atex2-0bOLDN  37230  isltrn2N  37271  cdleme0nex  37441  cdleme22b  37492  cdlemg17pq  37823  cdlemg19  37835  cdlemg21  37837  cdlemg33d  37860  dibopelvalN  38294  dibopelval2  38296  dib1dim  38316  dicelval2N  38333  diclspsn  38345  lcdlss  38770  mapd1o  38799  mzpcompact2lem  39397  fz1eqin  39415  rexrabdioph  39440  expdiophlem1  39667  dford4  39675  fnwe2lem2  39700  fgraphopab  39859  ifpidg  39906  rp-fakeinunass  39930  rp-isfinite6  39933  dfsucon  39938  elinintrab  39986  elnonrel  39994  elmapintab  40005  dfrtrcl5  40038  imaiun1  40045  coiun1  40046  rfovcnvf1od  40399  andi3or  40421  uneqsn  40422  ntrneicls00  40488  rr-groth  40684  2sbc5g  40797  pm14.12  40802  2sb5nd  40943  uun2221  41196  uun2221p1  41197  uun2221p2  41198  2sb5ndVD  41293  2sb5ndALT  41315  disjinfi  41503  climuz  42074  dfxlim2  42178  cncfshift  42206  dvnmul  42277  dvnprodlem2  42281  ismbl3  42320  ismbl4  42327  stoweidlem26  42360  stoweidlem35  42369  fourierdlem54  42494  fourierdlem83  42523  fourierdlem100  42540  fourierdlem104  42544  fourierdlem109  42549  fourierdlem112  42552  smfpimcc  43131  2reu8i  43361  dfdfat2  43376  ffnaov  43447  an4com24  43516  4an21  43518  iccpartiltu  43631  prproropf1olem0  43713  isrnghm  44212  2zrngmmgm  44266  rngcinv  44301  rngcinvALTV  44313  ringcinv  44352  ringcinvALTV  44376  opeliun2xp  44430  pgrpgt2nabl  44463  islindeps  44557  lindslinindsimp1  44561  lindslinindsimp2  44567  ldepslinc  44613  blen1b  44697  dffun3f  44834  setrec1lem3  44841  elpglem3  44864  elpg  44865