Theorem anbi2i 726

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anbi12i  729  bianass  838  an4  861  an42  862  anandir  868  dfbi3  933  dn1  1000  dfifp3  1009  an3andi  1437  an33rean  1438  anxordi  1471  cadcoma  1542  nic-mpALT  1588  nic-axALT  1590  19.27v  1895  19.41v  1901  3exdistr  1910  4exdistr  1911  19.27  2082  19.41  2090  19.27OLD  2222  sbn  2379  2sb5  2431  eu5  2484  eu3v  2486  eu2  2497  mo4f  2504  eu4  2506  2mos  2540  2eu4  2544  rexbii  3023  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  reu2  3361  reu6  3362  reu4  3367  reu7  3368  2reu5lem3  3382  2reu5  3383  rmo3  3494  dfpss2  3654  difdif  3698  raldifb  3712  inass  3785  dfss4  3820  dfin2  3822  indi  3832  indifdir  3842  undif3  3847  difin0ss  3900  inssdif0  3901  ssunpr  4305  unipr  4385  uniun  4392  uniin  4393  csbuni  4402  iunin2  4520  iundif2  4523  iindif2  4525  iinin2  4526  axrep1  4700  axrep4  4703  notzfaus  4766  reusv2lem4  4798  eqvinop  4881  opcom  4890  opeqsn  4892  snopeqop  4894  fconstmpt  5085  opeliunxp  5093  xpundi  5094  elvvv  5101  xpiindi  5179  elcnv2  5222  cnvuni  5231  dmuni  5256  opelres  5322  elima3  5392  imai  5397  imainss  5467  difxp  5477  xpdifid  5481  ssrnres  5491  mptpreima  5545  coundir  5554  rnco  5558  coass  5571  relrelss  5576  wfi  5630  ordtri3or  5672  dffun2  5814  dffun3  5815  dffun4  5816  dffun5  5817  dffun6f  5818  dffun7  5830  dffun8  5831  dffun9  5832  svrelfun  5875  fncnv  5876  imadif  5887  dfmpt3  5927  fint  5997  fin  5998  dff12  6013  fores  6037  dff1o4  6058  eqfnfv3  6221  fndmin  6232  fniniseg  6246  unpreima  6249  ffnfvf  6296  fsn2  6309  tpres  6371  fconstfv  6381  dff13f  6417  dff14a  6427  dff14b  6428  isocnv2  6481  ffnov  6662  eqfnov  6664  foov  6706  uniuni  6865  tfindsg  6952  findsg  6985  funcnvuni  7012  opabex3d  7037  opabex3  7038  frxp  7174  soxp  7177  suppvalbr  7186  mpt2xopovel  7233  brtpos  7248  tpostpos  7259  dfsmo2  7331  dfrecs3  7356  rdglem1  7398  tz7.49  7427  brwitnlem  7474  oeeu  7570  erinxp  7708  mapsncnv  7790  cbvixp  7811  ixpin  7819  ixpiin  7820  mptelixpg  7831  elixpsn  7833  ixpsnf1o  7834  mapsnen  7920  xpassen  7939  omxpenlem  7946  sbthcl  7967  wemapsolem  8338  dford2  8400  inf2  8403  zfinf  8419  trcl  8487  iscard2  8685  leweon  8717  aceq1  8823  dfac3  8827  dfac4  8828  dfac5lem2  8830  dfac5lem3  8831  dfac5  8834  kmlem3  8857  kmlem4  8858  kmlem14  8868  kmlem15  8869  dfackm  8871  infmap2  8923  cf0  8956  fin23lem25  9029  zorn2lem7  9207  brdom6disj  9235  zfcndrep  9315  zfcndinf  9319  fpwwe  9347  axgroth4  9533  grothprim  9535  grothtsk  9536  nqpr  9715  addsrmo  9773  mulsrmo  9774  opelreal  9830  elnnz  11264  elznn0nn  11268  peano2uz2  11341  nnwos  11631  dflt2  11857  xmullem  11966  elfzuzb  12207  4fvwrd4  12328  preduz  12330  elfznelfzo  12439  fzind2  12448  fsuppmapnn0fiubex  12654  hashinfxadd  13035  hashfun  13084  fi1uzind  13134  brfi1uzind  13135  opfi1uzind  13138  fi1uzindOLD  13140  brfi1uzindOLD  13141  opfi1uzindOLD  13144  cotr2g  13563  shftdm  13659  rexfiuz  13935  cbvsum  14273  mertenslem2  14456  mertens  14457  cbvprod  14484  prodmo  14505  iprodmul  14573  divalglem10  14963  ndvdssub  14971  bitsmod  14996  algcvgblem  15128  isprm2  15233  isprm4  15235  hashdvds  15318  infpn2  15455  hashbc0  15547  xpscf  16049  funcpropd  16383  isffth2  16399  eldmcoa  16538  setcinv  16563  xpccatid  16651  yonedainv  16744  ispos  16770  ispos2  16771  joinfval2  16825  meetfval2  16839  istsr2  17041  isnsg2  17447  isnsg4  17460  isgim  17527  oppgid  17609  oppgcntz  17617  symgfix2  17659  efgval2  17960  iscyg2  18107  dmdprdd  18221  subgdmdprd  18256  issrg  18330  oppr1  18457  opprunit  18484  opprirred  18525  isrhm  18544  subsubrg2  18630  islmim  18883  lbsextg  18983  lidlnz  19049  isdomn2  19120  opsrtoslem1  19305  resubdrg  19773  unocv  19843  pjfval2  19872  islinds2  19971  mdetunilem8  20244  fvmptnn04if  20473  istop2g  20526  isbasis2g  20563  tgval2  20571  isclo2  20702  isnrm2  20972  is1stc2  21055  llyi  21087  isfbas2  21449  elfg  21485  ufinffr  21543  isfcls  21623  alexsubALTlem2  21662  alexsubALTlem3  21663  cnextcn  21681  ustfilxp  21826  iscusp2  21916  elcncf1di  22506  isclmp  22705  iscvsp  22736  tchcph  22844  iscau3  22884  caucfil  22889  ellogdm  24185  dvdsflsumcom  24714  logfac2  24742  dchrelbas3  24763  dchrvmasumlema  24989  legtrid  25286  outpasch  25447  axcontlem5  25648  axcontlem6  25649  axcontlem7  25650  nb3grapr2  25983  uvtx01vtx  26020  3v3e3cycl2  26192  wwlkn0s  26233  wwlkextwrd  26256  wwlkextinj  26258  usg2spthonot0  26416  rusgranumwlkl1  26474  frgra3v  26529  4cycl2vnunb  26544  usg2spot2nb  26592  numclwwlkovf2  26611  numclwwlk3lem  26635  hhcms  27444  isch3  27482  ocsh  27526  pjhtheu  27637  pjpreeq  27641  h1deoi  27792  h1dei  27793  eleigvec  28200  cvbr2  28526  cvnbtwn2  28530  cvnbtwn4  28532  mdsl2i  28565  cvmdi  28567  mdsymlem6  28651  cdj3lem3b  28683  mo5f  28708  nmo  28709  rexunirn  28715  rmo3f  28719  rmo4fOLD  28720  rmo4f  28721  disjunsn  28789  unipreima  28826  dfcnv2  28859  1stpreima  28867  isrnsigaOLD  29502  isrnsiga  29503  rossros  29570  omsmeas  29712  eulerpartlemr  29763  eulerpartlemgvv  29765  ballotlemodife  29886  plymulx  29951  signstfvneq0  29975  bnj251  30021  bnj252  30022  bnj257  30026  bnj290  30029  bnj1304  30144  bnj153  30204  bnj543  30217  bnj571  30230  bnj580  30237  bnj607  30240  bnj882  30250  bnj964  30267  bnj996  30279  bnj1033  30291  bnj1176  30327  bnj1186  30329  bnj1189  30331  bnj1204  30334  bnj1253  30339  bnj1452  30374  bnj1463  30377  erdszelem9  30435  cvmlift2lem9  30547  cvmlift2lem13  30551  elmthm  30727  axinfprim  30837  axacprim  30838  coep  30894  dfso2  30897  fv1stcnv  30925  fv2ndcnv  30926  dford5reg  30931  dfon2lem5  30936  dfon2  30941  trpredmintr  30975  frind  30984  frr3g  31023  brtxp2  31158  brpprod3a  31163  dfom5b  31189  brcart  31209  brimg  31214  funpartlem  31219  dfrecs2  31227  cgrxfr  31332  segletr  31391  trer  31480  fneval  31517  neifg  31536  df3nandALT1  31566  andnand1  31568  nandsym1  31591  bj-dfssb2  31829  bj-axrep1  31976  bj-axrep4  31979  bj-eu3f  32017  bj-csbsnlem  32090  bj-snsetex  32144  bj-elsngl  32149  bj-snglc  32150  bj-restuni  32231  bj-sspwpw  32238  bj-dfmpt2a  32252  mptsnunlem  32361  icorempt2  32375  isbasisrelowllem2  32380  relowlpssretop  32388  rdgeqoa  32394  dffinxpf  32398  curf  32557  finixpnum  32564  ptrest  32578  poimirlem1  32580  poimirlem14  32593  poimirlem16  32595  poimirlem19  32598  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimir  32612  cnambfre  32628  itg2addnc  32634  ftc1anc  32663  opropabco  32688  f1opr  32689  isdrngo1  32925  keridl  33001  ispridlc  33039  selconj  33072  prtlem70  33157  prtlem100  33161  prtlem15  33178  islshpat  33322  lcvbr2  33327  lcvbr3  33328  lcvnbtwn2  33332  ellkr  33394  cvrval2  33579  cvrnbtwn2  33580  cvrnbtwn3  33581  cvrnbtwn4  33584  ishlat2  33658  lplnexatN  33867  islvol5  33883  dath  34040  pmapglb  34074  polval2N  34210  pclfinclN  34254  lhpexle3  34316  4atex2  34381  4atex2-0bOLDN  34383  isltrn2N  34424  cdleme0nex  34595  cdleme22b  34647  cdlemg17pq  34978  cdlemg19  34990  cdlemg21  34992  cdlemg33d  35015  dibopelvalN  35450  dibopelval2  35452  dib1dim  35472  dicelval2N  35489  diclspsn  35501  lcdlss  35926  mapd1o  35955  mzpcompact2lem  36332  fz1eqin  36350  rexrabdioph  36376  expdiophlem1  36606  dford4  36614  fnwe2lem2  36639  fgraphopab  36807  ifpidg  36855  rp-fakenanass  36879  rp-fakeinunass  36880  rp-isfinite6  36883  elinintrab  36902  elnonrel  36910  elmapintab  36921  dfrtrcl5  36955  imaiun1  36962  coiun1  36963  rfovcnvf1od  37318  andi3or  37340  uneqsn  37341  ntrneicls00  37407  2sbc5g  37639  pm14.12  37644  2sb5nd  37797  uun2221  38061  uun2221p1  38062  uun2221p2  38063  2sb5ndVD  38168  2sb5ndALT  38190  disjinfi  38375  cncfshift  38759  dvnmul  38833  dvnprodlem2  38837  ismbl3  38879  ismbl4  38886  stoweidlem26  38919  stoweidlem35  38928  fourierdlem54  39053  fourierdlem83  39082  fourierdlem100  39099  fourierdlem104  39103  fourierdlem109  39108  fourierdlem112  39111  reuan  39829  2reu4a  39838  dfdfat2  39860  ffnaov  39928  iccpartiltu  39960  rexdifpr  40315  nb3grpr2  40611  pthdlem1  40972  wwlksnextinj  41105  usgr2wspthon  41168  rusgrnumwwlkl1  41172  isclwwlks  41188  iseupthf1o  41369  frgr3v  41445  4cycl2vnunb-av  41460  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  av-numclwwlkovf2  41515  av-numclwwlk3lem  41538  isrnghm  41682  2zrngmmgm  41736  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  opeliun2xp  41904  pgrpgt2nabl  41941  islindeps  42036  lindslinindsimp1  42040  lindslinindsimp2  42046  ldepslinc  42092  blen1b  42180  dffun3f  42227  setrec1lem3  42235  elpglem3  42255  elpg  42256