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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anbi1ci  627  anbi12i  628  bianass  641  an42  656  anandir  676  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  an3andi  1483  an33rean  1484  an33reanOLD  1485  anxordi  1527  cadcoma  1614  nic-mpALT  1675  nic-axALT  1677  3exdistr  1965  4exdistr  1966  19.27v  1994  19.27  2221  19.41  2229  2sb5  2272  dfsb7  2276  dfeumo  2532  mo4f  2562  eu3v  2565  eu6  2569  dfeu  2590  eu2  2606  eu4  2612  2mos  2646  2eu4  2651  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  reu2  3721  reu6  3722  reu4  3727  reu7  3728  rmo3f  3730  rmo4f  3731  2reu5lem3  3753  2reu5  3754  sbcimdv  3851  sbcg  3856  rmo3  3883  reuan  3890  dfpss2  4085  difdif  4130  raldifb  4144  inass  4219  dfss4  4258  dfin2  4260  indi  4273  indifdi  4283  indifdirOLD  4285  undif3  4290  difin0ss  4368  inssdif0  4369  2nreu  4441  2reu4lem  4525  rexdifpr  4661  reuprg0  4706  ssdifsn  4791  ssunpr  4835  uniprg  4925  uniprOLD  4927  uniun  4934  uniin  4935  csbuni  4940  dfiun2g  5033  iunin2  5074  iundif2  5077  iindif2  5080  iinin2  5081  elpwpw  5105  axrep1  5286  axrep4  5290  reusv2lem4  5399  eqvinop  5487  opcom  5501  fconstmpt  5737  opeliunxp  5742  xpundi  5743  elvvv  5750  opelinxp  5754  xpiindi  5834  elcnv2  5876  cnvuni  5885  dmuni  5913  brres  5987  dmres  6002  elidinxp  6042  restidsing  6051  elima3  6065  asymref  6115  imainss  6151  difxp  6161  xpdifid  6165  mptpreima  6235  coundir  6245  resco  6247  coass  6262  relrelss  6270  opreu2reurex  6291  dfpo2  6293  frpoind  6341  wfiOLD  6350  ordtri3or  6394  dffun2  6551  dffun2OLD  6552  dffun2OLDOLD  6553  dffun6  6554  dffun3  6555  dffun3OLD  6556  dffun4  6557  dffun5  6558  dffun6f  6559  dffun7  6573  dffun8  6574  dffun9  6575  svrelfun  6618  fncnv  6619  imadif  6630  dfmpt3  6682  fcnvres  6766  fint  6768  fin  6769  dff12  6784  fores  6813  dff1o4  6839  eqfnfv3  7032  fndmin  7044  fniniseg  7059  unpreima  7062  ffnfvf  7116  fsn2  7131  tpres  7199  fconstfv  7211  dff13f  7252  dff14a  7266  dff14b  7267  isocnv2  7325  f1opr  7462  eloprabga  7513  ffnov  7532  eqfnov  7535  foov  7578  uniuni  7746  tfindsg  7847  findsg  7887  funcnvuni  7919  opabex3d  7949  opabex3rd  7950  opabex3  7951  1stconst  8083  2ndconst  8084  frxp  8109  soxp  8112  xpord3lem  8132  suppvalbr  8147  suppofssd  8185  suppcoss  8189  mpoxopovel  8202  brtpos  8217  tpostpos  8228  dfsmo2  8344  dfrecs3  8369  dfrecs3OLD  8370  rdglem1  8412  tz7.49  8442  brwitnlem  8504  oeeu  8600  naddasslem2  8691  erinxp  8782  mapsncnv  8884  cbvixp  8905  ixpin  8914  ixpiin  8915  mptelixpg  8926  elixpsn  8928  ixpsnf1o  8929  xpassen  9063  omxpenlem  9070  sbthcl  9092  sbthfilem  9198  wemapsolem  9542  dford2  9612  inf2  9615  zfinf  9631  ttrclselem2  9718  trcl  9720  frind  9742  frr3g  9748  iscard2  9968  leweon  10003  aceq1  10109  dfac3  10113  dfac4  10114  dfac5lem2  10116  dfac5  10120  kmlem3  10144  kmlem4  10145  kmlem14  10155  kmlem15  10156  dfackm  10158  infmap2  10210  fin23lem25  10316  zorn2lem7  10494  brdom6disj  10524  zfcndrep  10606  zfcndinf  10610  fpwwe  10638  axgroth4  10824  grothprim  10826  grothtsk  10827  nqpr  11006  addsrmo  11065  mulsrmo  11066  opelreal  11122  elnnz  12565  elznn0nn  12569  peano2uz2  12647  nnwos  12896  dflt2  13124  xmullem  13240  4fvwrd4  13618  preduz  13620  elfznelfzo  13734  fzind2  13747  fsuppmapnn0fiubex  13954  hashinfxadd  14342  hashgt23el  14381  hashfun  14394  fi1uzind  14455  brfi1uzind  14456  opfi1uzind  14459  cotr2g  14920  shftdm  15015  rexfiuz  15291  cbvsum  15638  mertenslem2  15828  mertens  15829  cbvprod  15856  prodmo  15877  iprodmul  15944  divalglem10  16342  ndvdssub  16349  bitsmod  16374  algcvgblem  16511  isprm2  16616  isprm4  16618  hashdvds  16705  infpn2  16843  hashbc0  16935  xpscf  17508  funcpropd  17848  isffth2  17864  eldmcoa  18012  setcinv  18037  xpccatid  18137  yonedainv  18231  ispos  18264  ispos2  18265  joinfval2  18324  meetfval2  18338  istsr2  18534  isnsg2  19031  isnsg4  19042  isgim  19131  oppgid  19218  oppgcntz  19226  symgfix2  19279  efgval2  19587  iscyg2  19745  dmdprdd  19864  subgdmdprd  19899  issrg  20005  oppr1  20157  opprunit  20184  opprirred  20229  isrhm  20250  subsubrg2  20384  islmim  20666  lbsextg  20768  lidlnz  20846  isdomn2  20908  resubdrg  21153  unocv  21225  pjfval2  21256  islinds2  21360  opsrtoslem1  21608  mdetunilem8  22113  istop2g  22390  isbasis2g  22443  tgval2  22451  isclo2  22584  isnrm2  22854  is1stc2  22938  llyi  22970  isfbas2  23331  elfg  23367  ufinffr  23425  isfcls  23505  alexsubALTlem2  23544  alexsubALTlem3  23545  cnextcn  23563  ustfilxp  23709  iscusp2  23799  metustid  24055  isclmp  24605  iscvsp  24636  tcphcph  24746  iscau3  24787  caucfil  24792  mdegleb  25574  ellogdm  26139  dvdsflsumcom  26682  logfac2  26710  dchrelbas3  26731  dchrvmasumlema  26993  nosupno  27196  noinfno  27211  noinfbnd1lem1  27216  dmscut  27302  made0  27358  mulsproplem5  27566  norecdiv  27628  legtrid  27832  outpasch  27996  axcontlem5  28216  axcontlem6  28217  axcontlem7  28218  nb3grpr2  28630  iscplgr  28662  pthdlem1  29013  wwlksnextinj  29143  usgr2wspthon  29209  rusgrnumwwlkl1  29212  isclwwlk  29227  clwwlkccatlem  29232  clwwlknon2x  29346  iseupthf1o  29445  frcond3  29512  frgr3v  29518  4cycl2vnunb  29533  frgrncvvdeqlem2  29543  fusgr2wsp2nb  29577  numclwlk1lem1  29612  hhcms  30444  isch3  30482  ocsh  30524  pjhtheu  30635  pjpreeq  30639  h1deoi  30790  h1dei  30791  eleigvec  31198  cvbr2  31524  cvnbtwn2  31528  cvnbtwn4  31530  mdsl2i  31563  cvmdi  31565  mdsymlem6  31649  cdj3lem3b  31681  mo5f  31717  nmo  31718  rexunirn  31720  dmrab  31725  difrab2  31726  disjunsn  31813  unipreima  31857  dfcnv2  31889  1stpreima  31916  lsmsnorb2  32491  prmidl0  32558  ssmxidl  32579  ressply1mon1p  32646  zarcls  32843  rhmpreimacnlem  32853  isrnsiga  33100  rossros  33167  omsmeas  33311  eulerpartlemr  33362  eulerpartlemgvv  33364  ballotlemodife  33485  plymulx  33548  signstfvneq0  33572  bnj251  33702  bnj252  33703  bnj257  33707  bnj290  33710  bnj1304  33819  bnj153  33880  bnj543  33893  bnj571  33906  bnj580  33913  bnj607  33916  bnj882  33926  bnj964  33943  bnj996  33956  bnj1033  33969  bnj1176  34005  bnj1186  34007  bnj1189  34009  bnj1204  34012  bnj1253  34017  bnj1452  34052  bnj1463  34055  dff15  34076  fineqvrep  34084  fineqvac  34086  lfuhgr3  34099  cusgredgex2  34102  usgrgt2cycl  34110  2cycl2d  34119  dfacycgr1  34124  erdszelem9  34179  cvmlift2lem9  34291  cvmlift2lem13  34295  satfvsucsuc  34345  satfdm  34349  satf0  34352  fmlasucdisj  34379  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  elmthm  34556  axinfprim  34664  axacprim  34665  xpab  34684  dfso2  34714  dford5reg  34743  dfon2lem5  34748  dfon2  34753  brtxp2  34842  brpprod3a  34847  dfom5b  34873  brcart  34893  brimg  34898  funpartlem  34903  dfrecs2  34911  cgrxfr  35016  segletr  35075  trer  35190  fneval  35226  neifg  35245  df3nandALT1  35273  andnand1  35275  nandsym1  35296  bj-eu3f  35709  bj-csbsnlem  35772  bj-snsetex  35833  bj-elsngl  35838  bj-snglc  35839  bj-restuni  35967  bj-dfmpoa  35988  bj-imdirco  36060  mptsnunlem  36208  icorempo  36221  isbasisrelowllem2  36226  relowlpssretop  36234  rdgeqoa  36240  difunieq  36244  dffinxpf  36255  nlpineqsn  36278  curf  36455  finixpnum  36462  ptrest  36476  poimirlem1  36478  poimirlem14  36491  poimirlem16  36493  poimirlem19  36496  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  poimir  36510  cnambfre  36525  itg2addnc  36531  ftc1anc  36558  opropabco  36581  isdrngo1  36813  keridl  36889  ispridlc  36927  selconj  36957  eldmqsres  37144  cnvepres  37156  ecinn0  37211  alrmomorn  37216  moantr  37222  dfxrn2  37235  disjressuc2  37247  inxpxrn  37254  rnxrnres  37258  coss2cnvepres  37277  refrelredund4  37494  dferALTV2  37527  dfeldisj3  37578  dfpart2  37628  prtlem70  37716  prtlem100  37718  prtlem15  37734  islshpat  37876  lcvbr2  37881  lcvbr3  37882  lcvnbtwn2  37886  ellkr  37948  cvrval2  38133  cvrnbtwn2  38134  cvrnbtwn3  38135  cvrnbtwn4  38138  ishlat2  38212  lplnexatN  38423  islvol5  38439  dath  38596  pclfinclN  38810  lhpexle3  38872  4atex2  38937  4atex2-0bOLDN  38939  isltrn2N  38980  cdleme0nex  39150  cdleme22b  39201  cdlemg17pq  39532  cdlemg19  39544  cdlemg21  39546  cdlemg33d  39569  dibopelvalN  40003  dibopelval2  40005  dib1dim  40025  dicelval2N  40042  diclspsn  40054  lcdlss  40479  mapd1o  40508  3factsumint2  40876  3factsumint3  40877  3factsumint  40879  sticksstones16  40967  sticksstones21  40972  metakunt1  40974  mzpcompact2lem  41475  fz1eqin  41493  rexrabdioph  41518  expdiophlem1  41746  dford4  41754  fnwe2lem2  41779  fgraphopab  41938  dflim6  42000  onsucf1olem  42006  onsucrn  42007  nnoeomeqom  42048  faosnf0.11b  42164  ifpidg  42228  rp-fakeinunass  42252  rp-isfinite6  42255  dfsucon  42260  elinintrab  42314  elnonrel  42322  elmapintab  42333  dfrtrcl5  42366  imaiun1  42388  coiun1  42389  rfovcnvf1od  42741  andi3or  42761  uneqsn  42762  ntrneicls00  42826  rr-groth  43044  ismnushort  43046  rr-grothshortbi  43048  2sbc5g  43161  pm14.12  43166  2sb5nd  43307  uun2221  43560  uun2221p1  43561  uun2221p2  43562  2sb5ndVD  43657  2sb5ndALT  43679  iindif2f  43840  disjinfi  43877  climuz  44447  dfxlim2  44551  cncfshift  44577  dvnmul  44646  dvnprodlem2  44650  ismbl3  44689  ismbl4  44696  stoweidlem26  44729  stoweidlem35  44738  fourierdlem54  44863  fourierdlem83  44892  fourierdlem100  44909  fourierdlem104  44913  fourierdlem109  44918  fourierdlem112  44921  smfpimcc  45511  fcoresf1ob  45770  f1cof1b  45772  f1ocof1ob  45776  2reu8i  45808  dfdfat2  45823  ffnaov  45894  an4com24  45963  4an21  45965  iccpartiltu  46077  prproropf1olem0  46157  isrnghm  46676  issubrng  46711  subsubrng2  46728  2zrngmmgm  46798  rngcinv  46833  rngcinvALTV  46845  ringcinv  46884  ringcinvALTV  46908  opeliun2xp  46962  pgrpgt2nabl  46996  islindeps  47088  lindslinindsimp1  47092  lindslinindsimp2  47098  ldepslinc  47144  blen1b  47228  i0oii  47506  io1ii  47507  iscnrm3lem3  47522  isthinc2  47596  isthinc3  47597  isthincd2  47612  dffun3f  47681  setrec1lem3  47688  elpglem3  47712  elpg  47713