Theorem anbi2i 623

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi1ci  626  anbi12i  628  bianass  642  an42  657  anandir  677  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1526  cadcoma  1612  nic-mpALT  1672  nic-axALT  1674  3exdistr  1960  4exdistr  1961  19.27v  1989  19.27  2227  19.41  2235  2sb5  2278  dfsb7  2279  dfeumo  2536  mo4f  2566  eu3v  2569  eu6  2573  dfeu  2594  eu2  2608  eu4  2614  2mos  2648  2mosOLD  2649  2eu4  2654  r3ex  3183  ceqsex3v  3516  ceqsex4v  3517  ceqsex8v  3519  reu2  3708  reu6  3709  reu4  3714  reu7  3715  rmo3f  3717  rmo4f  3718  2reu5lem3  3740  2reu5  3741  sbcimdv  3834  sbcg  3838  rmo3  3864  reuan  3871  dfpss2  4063  difdif  4110  raldifb  4124  inass  4203  dfss4  4244  dfin2  4246  indi  4259  indifdi  4269  undif3  4275  difin0ss  4348  inssdif0  4349  2nreu  4419  2reu4lem  4497  rexdifpr  4635  reuprg0  4678  ssdifsn  4764  ssunpr  4810  uniprg  4899  uniun  4906  uniin  4907  csbuni  4912  dfiun2g  5006  iunin2  5047  iundif2  5050  iindif2  5053  iinin2  5054  elpwpw  5078  axrep1  5250  axrep4v  5254  axrep4  5255  axrep4OLD  5256  reusv2lem4  5371  eqvinop  5462  opcom  5476  fconstmpt  5716  opeliunxp  5721  opeliun2xp  5722  xpundi  5723  elvvv  5730  opelinxp  5734  xpiindi  5815  elcnv2  5857  cnvuni  5866  dmuni  5894  brres  5973  dmres  5999  elidinxp  6031  restidsing  6040  elima3  6054  asymref  6105  imainss  6143  difxp  6153  xpdifid  6157  mptpreima  6227  coundir  6237  resco  6239  coass  6254  relrelss  6262  opreu2reurex  6283  dfpo2  6285  frpoind  6331  wfiOLD  6340  ordtri3or  6384  dffun2  6540  dffun2OLD  6541  dffun2OLDOLD  6542  dffun6  6543  dffun3  6544  dffun3OLD  6545  dffun4  6546  dffun5  6547  dffun6f  6548  dffun7  6562  dffun8  6563  dffun9  6564  svrelfun  6607  fncnv  6608  imadif  6619  dfmpt3  6671  fcnvres  6754  fint  6756  fin  6757  dff12  6772  fores  6799  dff1o4  6825  eqfnfv3  7022  fndmin  7034  fniniseg  7049  unpreima  7052  ffnfvf  7109  fsn2  7125  tpres  7192  fconstfv  7203  dff13f  7247  dff14a  7262  dff14b  7263  isocnv2  7323  f1opr  7461  eloprabga  7514  ffnov  7531  eqfnov  7534  foov  7579  uniuni  7754  tfindsg  7854  findsg  7891  funcnvuni  7926  opabex3d  7962  opabex3rd  7963  opabex3  7964  1stconst  8097  2ndconst  8098  frxp  8123  soxp  8126  xpord3lem  8146  suppvalbr  8161  suppofssd  8200  suppcoss  8204  mpoxopovel  8217  brtpos  8232  tpostpos  8243  dfsmo2  8359  dfrecs3  8384  dfrecs3OLD  8385  rdglem1  8427  tz7.49  8457  brwitnlem  8517  oeeu  8613  naddasslem2  8705  brinxper  8746  erinxp  8803  mapsncnv  8905  cbvixp  8926  cbvixpv  8927  ixpin  8935  ixpiin  8936  mptelixpg  8947  elixpsn  8949  ixpsnf1o  8950  xpassen  9078  omxpenlem  9085  sbthcl  9107  sbthfilem  9210  wemapsolem  9562  dford2  9632  inf2  9635  zfinf  9651  ttrclselem2  9738  trcl  9740  frind  9762  frr3g  9768  iscard2  9988  leweon  10023  aceq1  10129  dfac3  10133  dfac4  10134  dfac5lem2  10136  dfac5  10141  kmlem3  10165  kmlem4  10166  kmlem14  10176  kmlem15  10177  dfackm  10179  infmap2  10229  fin23lem25  10336  zorn2lem7  10514  brdom6disj  10544  zfcndrep  10626  zfcndinf  10630  fpwwe  10658  axgroth4  10844  grothprim  10846  grothtsk  10847  nqpr  11026  addsrmo  11085  mulsrmo  11086  opelreal  11142  elnnz  12596  elznn0nn  12600  peano2uz2  12679  nnwos  12929  dflt2  13162  xmullem  13278  4fvwrd4  13663  preduz  13665  elfznelfzo  13786  fzind2  13799  fsuppmapnn0fiubex  14008  hashinfxadd  14401  hashgt23el  14440  hashfun  14453  fi1uzind  14523  brfi1uzind  14524  opfi1uzind  14527  cotr2g  14993  shftdm  15088  rexfiuz  15364  cbvsum  15709  cbvsumv  15710  mertenslem2  15899  mertens  15900  cbvprod  15927  cbvprodv  15928  prodeq1i  15930  prodmo  15950  iprodmul  16017  divalglem10  16419  ndvdssub  16426  bitsmod  16453  algcvgblem  16594  isprm2  16699  isprm4  16701  hashdvds  16792  infpn2  16931  hashbc0  17023  xpscf  17577  funcpropd  17913  isffth2  17929  eldmcoa  18076  setcinv  18101  xpccatid  18198  yonedainv  18291  ispos  18324  ispos2  18325  joinfval2  18382  meetfval2  18396  istsr2  18592  isnsg2  19137  isnsg4  19148  isgim  19243  oppgid  19337  oppgcntz  19345  symgfix2  19395  efgval2  19703  iscyg2  19861  dmdprdd  19980  subgdmdprd  20015  issrg  20146  oppr1  20308  opprunit  20335  opprirred  20380  isrnghm  20399  isrhm  20436  issubrng  20505  subsubrng2  20522  subsubrg2  20557  rngcinv  20595  ringcinv  20629  isdomn2  20669  isdomn2OLD  20670  islmim  21018  lbsextg  21121  lidlnz  21201  resubdrg  21566  unocv  21638  pjfval2  21667  islinds2  21771  opsrtoslem1  22011  mdetunilem8  22555  istop2g  22832  isbasis2g  22884  tgval2  22892  isclo2  23024  isnrm2  23294  is1stc2  23378  llyi  23410  isfbas2  23771  elfg  23807  ufinffr  23865  isfcls  23945  alexsubALTlem2  23984  alexsubALTlem3  23985  cnextcn  24003  ustfilxp  24149  iscusp2  24238  metustid  24491  isclmp  25046  iscvsp  25077  tcphcph  25187  iscau3  25228  caucfil  25233  mdegleb  26019  ellogdm  26598  dvdsflsumcom  27148  logfac2  27178  dchrelbas3  27199  dchrvmasumlema  27461  nosupno  27665  noinfno  27680  noinfbnd1lem1  27685  dmscut  27773  made0  27829  mulsproplem5  28063  norecdiv  28133  elnnzs  28304  uzsind  28308  legtrid  28516  outpasch  28680  axcontlem5  28893  axcontlem6  28894  axcontlem7  28895  nb3grpr2  29308  iscplgr  29340  dfpth2  29657  pthdlem1  29694  wwlksnextinj  29827  usgr2wspthon  29893  rusgrnumwwlkl1  29896  isclwwlk  29911  clwwlkccatlem  29916  clwwlknon2x  30030  iseupthf1o  30129  frcond3  30196  frgr3v  30202  4cycl2vnunb  30217  frgrncvvdeqlem2  30227  fusgr2wsp2nb  30261  numclwlk1lem1  30296  hhcms  31130  isch3  31168  ocsh  31210  pjhtheu  31321  pjpreeq  31325  h1deoi  31476  h1dei  31477  eleigvec  31884  cvbr2  32210  cvnbtwn2  32214  cvnbtwn4  32216  mdsl2i  32249  cvmdi  32251  mdsymlem6  32335  cdj3lem3b  32367  mo5f  32416  nmo  32417  rexunirn  32419  dmrab  32424  difrab2  32425  disjunsn  32521  unipreima  32567  dfcnv2  32600  1stpreima  32630  isunit2  33181  lsmsnorb2  33353  prmidl0  33411  ssmxidl  33435  1arithufdlem4  33508  ressply1mon1p  33527  zarcls  33851  rhmpreimacnlem  33861  isrnsiga  34090  rossros  34157  omsmeas  34301  eulerpartlemr  34352  eulerpartlemgvv  34354  ballotlemodife  34476  plymulx  34526  signstfvneq0  34550  bnj251  34679  bnj252  34680  bnj257  34684  bnj290  34687  bnj1304  34796  bnj153  34857  bnj543  34870  bnj571  34883  bnj580  34890  bnj607  34893  bnj882  34903  bnj964  34920  bnj996  34933  bnj1033  34946  bnj1176  34982  bnj1186  34984  bnj1189  34986  bnj1204  34989  bnj1253  34994  bnj1452  35029  bnj1463  35032  dff15  35061  fineqvrep  35072  fineqvac  35074  lfuhgr3  35088  cusgredgex2  35091  usgrgt2cycl  35098  2cycl2d  35107  dfacycgr1  35112  erdszelem9  35167  cvmlift2lem9  35279  cvmlift2lem13  35283  satfvsucsuc  35333  satfdm  35337  satf0  35340  fmlasucdisj  35367  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  elmthm  35544  axinfprim  35669  axacprim  35670  xpab  35689  dfso2  35718  dford5reg  35746  dfon2lem5  35751  dfon2  35756  brtxp2  35845  brpprod3a  35850  dfom5b  35876  brcart  35896  brimg  35901  funpartlem  35906  dfrecs2  35914  cgrxfr  36019  segletr  36078  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36211  trer  36280  fneval  36316  neifg  36335  df3nandALT1  36363  andnand1  36365  nandsym1  36386  weiunlem2  36427  bj-eu3f  36805  bj-csbsnlem  36867  bj-snsetex  36927  bj-elsngl  36932  bj-snglc  36933  bj-restuni  37061  bj-dfmpoa  37082  bj-imdirco  37154  mptsnunlem  37302  icorempo  37315  isbasisrelowllem2  37320  relowlpssretop  37328  rdgeqoa  37334  difunieq  37338  dffinxpf  37349  nlpineqsn  37372  curf  37568  finixpnum  37575  ptrest  37589  poimirlem1  37591  poimirlem14  37604  poimirlem16  37606  poimirlem19  37609  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimir  37623  cnambfre  37638  itg2addnc  37644  ftc1anc  37671  opropabco  37694  isdrngo1  37926  keridl  38002  ispridlc  38040  selconj  38070  eldmqsres  38251  cnvepres  38262  ecinn0  38317  alrmomorn  38322  moantr  38328  dfxrn2  38340  disjressuc2  38352  inxpxrn  38359  rnxrnres  38363  coss2cnvepres  38382  refrelredund4  38599  dferALTV2  38632  dfeldisj3  38683  dfpart2  38733  prtlem70  38821  prtlem100  38823  prtlem15  38839  islshpat  38981  lcvbr2  38986  lcvbr3  38987  lcvnbtwn2  38991  ellkr  39053  cvrval2  39238  cvrnbtwn2  39239  cvrnbtwn3  39240  cvrnbtwn4  39243  ishlat2  39317  lplnexatN  39528  islvol5  39544  dath  39701  pclfinclN  39915  lhpexle3  39977  4atex2  40042  4atex2-0bOLDN  40044  isltrn2N  40085  cdleme0nex  40255  cdleme22b  40306  cdlemg17pq  40637  cdlemg19  40649  cdlemg21  40651  cdlemg33d  40674  dibopelvalN  41108  dibopelval2  41110  dib1dim  41130  dicelval2N  41147  diclspsn  41159  lcdlss  41584  mapd1o  41613  3factsumint2  41981  3factsumint3  41982  3factsumint  41984  hashnexinj  42087  sticksstones16  42121  sticksstones21  42126  unitscyglem3  42156  metakunt1  42164  supinf  42240  fimgmcyclem  42503  eu6w  42646  mzpcompact2lem  42721  fz1eqin  42739  rexrabdioph  42764  expdiophlem1  42992  dford4  43000  fnwe2lem2  43022  fgraphopab  43174  dflim6  43235  onsucf1olem  43241  onsucrn  43242  nnoeomeqom  43283  faosnf0.11b  43398  ifpidg  43462  rp-fakeinunass  43486  rp-isfinite6  43489  dfsucon  43494  elinintrab  43548  elnonrel  43556  elmapintab  43567  dfrtrcl5  43600  imaiun1  43622  coiun1  43623  rfovcnvf1od  43975  andi3or  43995  uneqsn  43996  ntrneicls00  44060  rr-groth  44271  ismnushort  44273  rr-grothshortbi  44275  2sbc5g  44388  pm14.12  44393  2sb5nd  44533  uun2221  44785  uun2221p1  44786  uun2221p2  44787  2sb5ndVD  44882  2sb5ndALT  44904  modelaxreplem3  44953  iindif2f  45132  disjinfi  45164  climuz  45721  dfxlim2  45825  cncfshift  45851  dvnmul  45920  dvnprodlem2  45924  ismbl3  45963  ismbl4  45970  stoweidlem26  46003  stoweidlem35  46012  fourierdlem54  46137  fourierdlem83  46166  fourierdlem100  46183  fourierdlem104  46187  fourierdlem109  46192  fourierdlem112  46195  smfpimcc  46785  fcoresf1ob  47050  f1cof1b  47054  f1ocof1ob  47058  2reu8i  47090  dfdfat2  47105  ffnaov  47176  an4com24  47245  4an21  47247  iccpartiltu  47384  prproropf1olem0  47464  dfgric2  47876  gpgvtxedg0  48015  gpgvtxedg1  48016  gpgprismgr4cycllem10  48051  2zrngmmgm  48175  rngcinvALTV  48199  ringcinvALTV  48233  pgrpgt2nabl  48289  islindeps  48377  lindslinindsimp1  48381  lindslinindsimp2  48387  ldepslinc  48433  blen1b  48516  coxp  48759  i0oii  48842  io1ii  48843  isthinc2  49254  isthinc3  49255  isthincd2  49271  istermc2  49309  istermc3  49310  dffun3f  49494  setrec1lem3  49501  elpglem3  49525  elpg  49526