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  anxordi  1515  norassOLD  1530  cadcoma  1609  nic-mpALT  1669  nic-axALT  1671  3exdistr  1958  4exdistr  1959  19.27v  1992  19.27  2224  19.41  2232  2sb5  2278  dfsb7  2281  dfsb7OLD  2282  sbnOLD  2537  sbnALT  2591  dfeumo  2615  mo4f  2647  eu3v  2651  eu6  2655  dfeu  2677  eu2  2689  eu4  2695  2mos  2730  2eu4  2737  rexbii  3247  ceqsex3v  3546  ceqsex4v  3547  ceqsex8v  3549  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  4592  reuprg0  4632  ssdifsn  4714  ssunpr  4759  unipr  4845  uniun  4851  uniin  4852  csbuni  4860  iunin2  4986  iundif2  4989  iindif2  4992  iinin2  4993  elpwpw  5017  axrep1  5184  axrep4  5188  notzfausOLD  5256  reusv2lem4  5294  eqvinop  5371  opcom  5384  fconstmpt  5609  opeliunxp  5614  xpundi  5615  elvvv  5622  opelinxp  5626  xpiindi  5701  elcnv2  5743  cnvuni  5752  dmuni  5778  brres  5855  dmres  5870  elidinxp  5906  restidsing  5917  elima3  5931  asymref  5971  imainss  6006  difxp  6016  xpdifid  6020  mptpreima  6087  coundir  6096  resco  6098  coass  6113  relrelss  6119  opreu2reurex  6140  wfi  6176  ordtri3or  6218  dffun2  6360  dffun3  6361  dffun4  6362  dffun5  6363  dffun6f  6364  dffun7  6377  dffun8  6378  dffun9  6379  svrelfun  6421  fncnv  6422  imadif  6433  dfmpt3  6477  fcnvres  6551  fint  6553  fin  6554  dff12  6569  fores  6595  dff1o4  6618  eqfnfv3  6799  fndmin  6810  fniniseg  6825  unpreima  6828  ffnfvf  6878  fsn2  6893  tpres  6958  fconstfv  6969  dff13f  7008  dff14a  7022  dff14b  7023  isocnv2  7078  f1opr  7204  ffnov  7272  eqfnov  7274  foov  7316  uniuni  7478  tfindsg  7569  findsg  7603  funcnvuni  7630  opabex3d  7660  opabex3rd  7661  opabex3  7662  1stconst  7789  2ndconst  7790  frxp  7814  soxp  7817  suppvalbr  7828  suppofssd  7861  mpoxopovel  7880  brtpos  7895  tpostpos  7906  dfsmo2  7978  dfrecs3  8003  rdglem1  8045  tz7.49  8075  brwitnlem  8126  oeeu  8223  erinxp  8365  mapsncnv  8451  cbvixp  8472  ixpin  8481  ixpiin  8482  mptelixpg  8493  elixpsn  8495  ixpsnf1o  8496  xpassen  8605  omxpenlem  8612  sbthcl  8633  wemapsolem  9008  dford2  9077  inf2  9080  zfinf  9096  trcl  9164  iscard2  9399  leweon  9431  aceq1  9537  dfac3  9541  dfac4  9542  dfac5lem2  9544  dfac5  9548  kmlem3  9572  kmlem4  9573  kmlem14  9583  kmlem15  9584  dfackm  9586  infmap2  9634  fin23lem25  9740  zorn2lem7  9918  brdom6disj  9948  zfcndrep  10030  zfcndinf  10034  fpwwe  10062  axgroth4  10248  grothprim  10250  grothtsk  10251  nqpr  10430  addsrmo  10489  mulsrmo  10490  opelreal  10546  elnnz  11985  elznn0nn  11989  peano2uz2  12064  nnwos  12309  dflt2  12535  xmullem  12651  4fvwrd4  13021  preduz  13023  elfznelfzo  13136  fzind2  13149  fsuppmapnn0fiubex  13354  hashinfxadd  13740  hashgt23el  13779  hashfun  13792  fi1uzind  13849  brfi1uzind  13850  opfi1uzind  13853  cotr2g  14330  shftdm  14424  rexfiuz  14701  cbvsum  15046  mertenslem2  15235  mertens  15236  cbvprod  15263  prodmo  15284  iprodmul  15351  divalglem10  15747  ndvdssub  15754  bitsmod  15779  algcvgblem  15915  isprm2  16020  isprm4  16022  hashdvds  16106  infpn2  16243  hashbc0  16335  xpscf  16832  funcpropd  17164  isffth2  17180  eldmcoa  17319  setcinv  17344  xpccatid  17432  yonedainv  17525  ispos  17551  ispos2  17552  joinfval2  17606  meetfval2  17620  istsr2  17822  isnsg2  18302  isnsg4  18313  isgim  18396  oppgid  18478  oppgcntz  18486  symgfix2  18538  efgval2  18844  iscyg2  18995  dmdprdd  19115  subgdmdprd  19150  issrg  19251  oppr1  19378  opprunit  19405  opprirred  19446  isrhm  19467  subsubrg2  19556  islmim  19828  lbsextg  19928  lidlnz  19995  isdomn2  20066  opsrtoslem1  20258  resubdrg  20746  unocv  20818  pjfval2  20847  islinds2  20951  mdetunilem8  21222  istop2g  21498  isbasis2g  21550  tgval2  21558  isclo2  21690  isnrm2  21960  is1stc2  22044  llyi  22076  isfbas2  22437  elfg  22473  ufinffr  22531  isfcls  22611  alexsubALTlem2  22650  alexsubALTlem3  22651  cnextcn  22669  ustfilxp  22815  iscusp2  22905  metustid  23158  isclmp  23695  iscvsp  23726  tcphcph  23834  iscau3  23875  caucfil  23880  ellogdm  25216  dvdsflsumcom  25759  logfac2  25787  dchrelbas3  25808  dchrvmasumlema  26070  legtrid  26371  outpasch  26535  axcontlem5  26748  axcontlem6  26749  axcontlem7  26750  nb3grpr2  27159  iscplgr  27191  pthdlem1  27541  wwlksnextinj  27671  usgr2wspthon  27738  rusgrnumwwlkl1  27741  isclwwlk  27756  clwwlkccatlem  27761  clwwlknon2x  27876  iseupthf1o  27975  frcond3  28042  frgr3v  28048  4cycl2vnunb  28063  frgrncvvdeqlem2  28073  fusgr2wsp2nb  28107  numclwlk1lem1  28142  hhcms  28974  isch3  29012  ocsh  29054  pjhtheu  29165  pjpreeq  29169  h1deoi  29320  h1dei  29321  eleigvec  29728  cvbr2  30054  cvnbtwn2  30058  cvnbtwn4  30060  mdsl2i  30093  cvmdi  30095  mdsymlem6  30179  cdj3lem3b  30211  mo5f  30247  nmo  30248  rexunirn  30250  dmrab  30254  difrab2  30255  disjunsn  30338  unipreima  30385  dfcnv2  30416  1stpreima  30436  ssmxidl  30974  isrnsiga  31367  rossros  31434  omsmeas  31576  eulerpartlemr  31627  eulerpartlemgvv  31629  ballotlemodife  31750  plymulx  31813  signstfvneq0  31837  bnj251  31967  bnj252  31968  bnj257  31972  bnj290  31975  bnj1304  32086  bnj153  32147  bnj543  32160  bnj571  32173  bnj580  32180  bnj607  32183  bnj882  32193  bnj964  32210  bnj996  32223  bnj1033  32236  bnj1176  32272  bnj1186  32274  bnj1189  32276  bnj1204  32279  bnj1253  32284  bnj1452  32319  bnj1463  32322  dff15  32348  lfuhgr3  32361  cusgredgex2  32364  usgrgt2cycl  32372  2cycl2d  32381  dfacycgr1  32386  erdszelem9  32441  cvmlift2lem9  32553  cvmlift2lem13  32557  satfvsucsuc  32607  satfdm  32611  satf0  32614  fmlasucdisj  32641  satffunlem  32643  satffunlem1lem1  32644  satffunlem2lem1  32646  elmthm  32818  axinfprim  32927  axacprim  32928  dfso2  32985  dfpo2  32986  dford5reg  33022  dfon2lem5  33027  dfon2  33032  trpredmintr  33065  frpoind  33075  frind  33080  frr3g  33116  nosupno  33198  dmscut  33267  brtxp2  33337  brpprod3a  33342  dfom5b  33368  brcart  33388  brimg  33393  funpartlem  33398  dfrecs2  33406  cgrxfr  33511  segletr  33570  trer  33659  fneval  33695  neifg  33714  df3nandALT1  33742  andnand1  33744  nandsym1  33765  bj-eu3f  34160  bj-csbsnlem  34215  bj-snsetex  34270  bj-elsngl  34275  bj-snglc  34276  bj-restuni  34382  bj-dfmpoa  34404  bj-isrvec  34569  mptsnunlem  34613  icorempo  34626  isbasisrelowllem2  34631  relowlpssretop  34639  rdgeqoa  34645  difunieq  34649  dffinxpf  34660  nlpineqsn  34683  wl-dfrabsb  34855  curf  34864  finixpnum  34871  ptrest  34885  poimirlem1  34887  poimirlem14  34900  poimirlem16  34902  poimirlem19  34905  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimir  34919  cnambfre  34934  itg2addnc  34940  ftc1anc  34969  opropabco  34993  isdrngo1  35228  keridl  35304  ispridlc  35342  selconj  35372  eldmqsres  35537  cnvepres  35549  ecinn0  35601  alrmomorn  35606  moantr  35610  dfxrn2  35622  inxpxrn  35637  rnxrnres  35641  refrelredund4  35864  dferALTV2  35896  dfeldisj3  35946  prtlem70  35987  prtlem100  35989  prtlem15  36005  islshpat  36147  lcvbr2  36152  lcvbr3  36153  lcvnbtwn2  36157  ellkr  36219  cvrval2  36404  cvrnbtwn2  36405  cvrnbtwn3  36406  cvrnbtwn4  36409  ishlat2  36483  lplnexatN  36693  islvol5  36709  dath  36866  pclfinclN  37080  lhpexle3  37142  4atex2  37207  4atex2-0bOLDN  37209  isltrn2N  37250  cdleme0nex  37420  cdleme22b  37471  cdlemg17pq  37802  cdlemg19  37814  cdlemg21  37816  cdlemg33d  37839  dibopelvalN  38273  dibopelval2  38275  dib1dim  38295  dicelval2N  38312  diclspsn  38324  lcdlss  38749  mapd1o  38778  mzpcompact2lem  39341  fz1eqin  39359  rexrabdioph  39384  expdiophlem1  39611  dford4  39619  fnwe2lem2  39644  fgraphopab  39803  ifpidg  39850  rp-fakeinunass  39874  rp-isfinite6  39877  dfsucon  39882  elinintrab  39930  elnonrel  39938  elmapintab  39949  dfrtrcl5  39982  imaiun1  39989  coiun1  39990  rfovcnvf1od  40343  andi3or  40365  uneqsn  40366  ntrneicls00  40432  rr-groth  40628  2sbc5g  40741  pm14.12  40746  2sb5nd  40887  uun2221  41140  uun2221p1  41141  uun2221p2  41142  2sb5ndVD  41237  2sb5ndALT  41259  disjinfi  41446  climuz  42017  dfxlim2  42121  cncfshift  42149  dvnmul  42220  dvnprodlem2  42224  ismbl3  42264  ismbl4  42271  stoweidlem26  42304  stoweidlem35  42313  fourierdlem54  42438  fourierdlem83  42467  fourierdlem100  42484  fourierdlem104  42488  fourierdlem109  42493  fourierdlem112  42496  smfpimcc  43075  2reu8i  43305  dfdfat2  43320  ffnaov  43391  an4com24  43460  4an21  43462  iccpartiltu  43575  prproropf1olem0  43657  isrnghm  44156  2zrngmmgm  44210  rngcinv  44245  rngcinvALTV  44257  ringcinv  44296  ringcinvALTV  44320  opeliun2xp  44374  pgrpgt2nabl  44407  islindeps  44501  lindslinindsimp1  44505  lindslinindsimp2  44511  ldepslinc  44557  blen1b  44641  dffun3f  44778  setrec1lem3  44785  elpglem3  44808  elpg  44809