Theorem anbi2i 622

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  625  anbi12i  627  bianass  641  an42  656  anandir  676  dfbi3  1050  dn1  1058  dfifp3  1066  ifpdfbi  1071  an3andi  1482  an33rean  1483  anxordi  1523  cadcoma  1609  nic-mpALT  1670  nic-axALT  1672  3exdistr  1960  4exdistr  1961  19.27v  1989  19.27  2228  19.41  2236  2sb5  2281  dfsb7  2283  dfeumo  2540  mo4f  2570  eu3v  2573  eu6  2577  dfeu  2598  eu2  2612  eu4  2618  2mos  2652  2mosOLD  2653  2eu4  2658  r3ex  3204  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  reu2  3747  reu6  3748  reu4  3753  reu7  3754  rmo3f  3756  rmo4f  3757  2reu5lem3  3779  2reu5  3780  sbcimdv  3878  sbcg  3883  rmo3  3911  reuan  3918  dfpss2  4111  difdif  4158  raldifb  4172  inass  4249  dfss4  4288  dfin2  4290  indi  4303  indifdi  4313  undif3  4319  difin0ss  4396  inssdif0  4397  2nreu  4467  2reu4lem  4545  rexdifpr  4681  reuprg0  4727  ssdifsn  4813  ssunpr  4859  uniprg  4947  uniun  4954  uniin  4955  csbuni  4960  dfiun2g  5053  iunin2  5094  iundif2  5097  iindif2  5100  iinin2  5101  elpwpw  5125  axrep1  5304  axrep4  5308  reusv2lem4  5419  eqvinop  5507  opcom  5520  fconstmpt  5762  opeliunxp  5767  xpundi  5768  elvvv  5775  opelinxp  5779  xpiindi  5860  elcnv2  5902  cnvuni  5911  dmuni  5939  brres  6016  dmres  6041  elidinxp  6073  restidsing  6082  elima3  6096  asymref  6148  imainss  6185  difxp  6195  xpdifid  6199  mptpreima  6269  coundir  6279  resco  6281  coass  6296  relrelss  6304  opreu2reurex  6325  dfpo2  6327  frpoind  6374  wfiOLD  6383  ordtri3or  6427  dffun2  6583  dffun2OLD  6584  dffun2OLDOLD  6585  dffun6  6586  dffun3  6587  dffun3OLD  6588  dffun4  6589  dffun5  6590  dffun6f  6591  dffun7  6605  dffun8  6606  dffun9  6607  svrelfun  6650  fncnv  6651  imadif  6662  dfmpt3  6714  fcnvres  6798  fint  6800  fin  6801  dff12  6816  fores  6844  dff1o4  6870  eqfnfv3  7066  fndmin  7078  fniniseg  7093  unpreima  7096  ffnfvf  7154  fsn2  7170  tpres  7238  fconstfv  7249  dff13f  7293  dff14a  7307  dff14b  7308  isocnv2  7367  f1opr  7506  eloprabga  7558  ffnov  7576  eqfnov  7579  foov  7624  uniuni  7797  tfindsg  7898  findsg  7937  funcnvuni  7972  opabex3d  8006  opabex3rd  8007  opabex3  8008  1stconst  8141  2ndconst  8142  frxp  8167  soxp  8170  xpord3lem  8190  suppvalbr  8205  suppofssd  8244  suppcoss  8248  mpoxopovel  8261  brtpos  8276  tpostpos  8287  dfsmo2  8403  dfrecs3  8428  dfrecs3OLD  8429  rdglem1  8471  tz7.49  8501  brwitnlem  8563  oeeu  8659  naddasslem2  8751  brinxper  8792  erinxp  8849  mapsncnv  8951  cbvixp  8972  cbvixpv  8973  ixpin  8981  ixpiin  8982  mptelixpg  8993  elixpsn  8995  ixpsnf1o  8996  xpassen  9132  omxpenlem  9139  sbthcl  9161  sbthfilem  9264  wemapsolem  9619  dford2  9689  inf2  9692  zfinf  9708  ttrclselem2  9795  trcl  9797  frind  9819  frr3g  9825  iscard2  10045  leweon  10080  aceq1  10186  dfac3  10190  dfac4  10191  dfac5lem2  10193  dfac5  10198  kmlem3  10222  kmlem4  10223  kmlem14  10233  kmlem15  10234  dfackm  10236  infmap2  10286  fin23lem25  10393  zorn2lem7  10571  brdom6disj  10601  zfcndrep  10683  zfcndinf  10687  fpwwe  10715  axgroth4  10901  grothprim  10903  grothtsk  10904  nqpr  11083  addsrmo  11142  mulsrmo  11143  opelreal  11199  elnnz  12649  elznn0nn  12653  peano2uz2  12731  nnwos  12980  dflt2  13210  xmullem  13326  4fvwrd4  13705  preduz  13707  elfznelfzo  13822  fzind2  13835  fsuppmapnn0fiubex  14043  hashinfxadd  14434  hashgt23el  14473  hashfun  14486  fi1uzind  14556  brfi1uzind  14557  opfi1uzind  14560  cotr2g  15025  shftdm  15120  rexfiuz  15396  cbvsum  15743  cbvsumv  15744  mertenslem2  15933  mertens  15934  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  prodmo  15984  iprodmul  16051  divalglem10  16450  ndvdssub  16457  bitsmod  16482  algcvgblem  16624  isprm2  16729  isprm4  16731  hashdvds  16822  infpn2  16960  hashbc0  17052  xpscf  17625  funcpropd  17967  isffth2  17983  eldmcoa  18132  setcinv  18157  xpccatid  18257  yonedainv  18351  ispos  18384  ispos2  18385  joinfval2  18444  meetfval2  18458  istsr2  18654  isnsg2  19196  isnsg4  19207  isgim  19302  oppgid  19399  oppgcntz  19407  symgfix2  19458  efgval2  19766  iscyg2  19924  dmdprdd  20043  subgdmdprd  20078  issrg  20215  oppr1  20376  opprunit  20403  opprirred  20448  isrnghm  20467  isrhm  20504  issubrng  20573  subsubrng2  20590  subsubrg2  20627  rngcinv  20659  ringcinv  20693  isdomn2  20733  isdomn2OLD  20734  islmim  21084  lbsextg  21187  lidlnz  21275  resubdrg  21649  unocv  21721  pjfval2  21752  islinds2  21856  opsrtoslem1  22102  mdetunilem8  22646  istop2g  22923  isbasis2g  22976  tgval2  22984  isclo2  23117  isnrm2  23387  is1stc2  23471  llyi  23503  isfbas2  23864  elfg  23900  ufinffr  23958  isfcls  24038  alexsubALTlem2  24077  alexsubALTlem3  24078  cnextcn  24096  ustfilxp  24242  iscusp2  24332  metustid  24588  isclmp  25149  iscvsp  25180  tcphcph  25290  iscau3  25331  caucfil  25336  mdegleb  26123  ellogdm  26699  dvdsflsumcom  27249  logfac2  27279  dchrelbas3  27300  dchrvmasumlema  27562  nosupno  27766  noinfno  27781  noinfbnd1lem1  27786  dmscut  27874  made0  27930  mulsproplem5  28164  norecdiv  28234  elnnzs  28405  uzsind  28409  legtrid  28617  outpasch  28781  axcontlem5  29001  axcontlem6  29002  axcontlem7  29003  nb3grpr2  29418  iscplgr  29450  pthdlem1  29802  wwlksnextinj  29932  usgr2wspthon  29998  rusgrnumwwlkl1  30001  isclwwlk  30016  clwwlkccatlem  30021  clwwlknon2x  30135  iseupthf1o  30234  frcond3  30301  frgr3v  30307  4cycl2vnunb  30322  frgrncvvdeqlem2  30332  fusgr2wsp2nb  30366  numclwlk1lem1  30401  hhcms  31235  isch3  31273  ocsh  31315  pjhtheu  31426  pjpreeq  31430  h1deoi  31581  h1dei  31582  eleigvec  31989  cvbr2  32315  cvnbtwn2  32319  cvnbtwn4  32321  mdsl2i  32354  cvmdi  32356  mdsymlem6  32440  cdj3lem3b  32472  mo5f  32517  nmo  32518  rexunirn  32520  dmrab  32525  difrab2  32526  disjunsn  32616  unipreima  32662  dfcnv2  32694  1stpreima  32718  isunit2  33220  lsmsnorb2  33385  prmidl0  33443  ssmxidl  33467  1arithufdlem4  33540  ressply1mon1p  33558  zarcls  33820  rhmpreimacnlem  33830  isrnsiga  34077  rossros  34144  omsmeas  34288  eulerpartlemr  34339  eulerpartlemgvv  34341  ballotlemodife  34462  plymulx  34525  signstfvneq0  34549  bnj251  34678  bnj252  34679  bnj257  34683  bnj290  34686  bnj1304  34795  bnj153  34856  bnj543  34869  bnj571  34882  bnj580  34889  bnj607  34892  bnj882  34902  bnj964  34919  bnj996  34932  bnj1033  34945  bnj1176  34981  bnj1186  34983  bnj1189  34985  bnj1204  34988  bnj1253  34993  bnj1452  35028  bnj1463  35031  dff15  35060  fineqvrep  35071  fineqvac  35073  lfuhgr3  35087  cusgredgex2  35090  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  35668  axacprim  35669  xpab  35688  dfso2  35717  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  36213  trer  36282  fneval  36318  neifg  36337  df3nandALT1  36365  andnand1  36367  nandsym1  36388  weiunlem2  36429  bj-eu3f  36807  bj-csbsnlem  36869  bj-snsetex  36929  bj-elsngl  36934  bj-snglc  36935  bj-restuni  37063  bj-dfmpoa  37084  bj-imdirco  37156  mptsnunlem  37304  icorempo  37317  isbasisrelowllem2  37322  relowlpssretop  37330  rdgeqoa  37336  difunieq  37340  dffinxpf  37351  nlpineqsn  37374  curf  37558  finixpnum  37565  ptrest  37579  poimirlem1  37581  poimirlem14  37594  poimirlem16  37596  poimirlem19  37599  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimir  37613  cnambfre  37628  itg2addnc  37634  ftc1anc  37661  opropabco  37684  isdrngo1  37916  keridl  37992  ispridlc  38030  selconj  38060  eldmqsres  38243  cnvepres  38254  ecinn0  38309  alrmomorn  38314  moantr  38320  dfxrn2  38332  disjressuc2  38344  inxpxrn  38351  rnxrnres  38355  coss2cnvepres  38374  refrelredund4  38591  dferALTV2  38624  dfeldisj3  38675  dfpart2  38725  prtlem70  38813  prtlem100  38815  prtlem15  38831  islshpat  38973  lcvbr2  38978  lcvbr3  38979  lcvnbtwn2  38983  ellkr  39045  cvrval2  39230  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrnbtwn4  39235  ishlat2  39309  lplnexatN  39520  islvol5  39536  dath  39693  pclfinclN  39907  lhpexle3  39969  4atex2  40034  4atex2-0bOLDN  40036  isltrn2N  40077  cdleme0nex  40247  cdleme22b  40298  cdlemg17pq  40629  cdlemg19  40641  cdlemg21  40643  cdlemg33d  40666  dibopelvalN  41100  dibopelval2  41102  dib1dim  41122  dicelval2N  41139  diclspsn  41151  lcdlss  41576  mapd1o  41605  3factsumint2  41979  3factsumint3  41980  3factsumint  41982  hashnexinj  42085  sticksstones16  42119  sticksstones21  42124  unitscyglem3  42154  metakunt1  42162  supinf  42237  fimgmcyclem  42488  eu6w  42631  mzpcompact2lem  42707  fz1eqin  42725  rexrabdioph  42750  expdiophlem1  42978  dford4  42986  fnwe2lem2  43008  fgraphopab  43164  dflim6  43226  onsucf1olem  43232  onsucrn  43233  nnoeomeqom  43274  faosnf0.11b  43389  ifpidg  43453  rp-fakeinunass  43477  rp-isfinite6  43480  dfsucon  43485  elinintrab  43539  elnonrel  43547  elmapintab  43558  dfrtrcl5  43591  imaiun1  43613  coiun1  43614  rfovcnvf1od  43966  andi3or  43986  uneqsn  43987  ntrneicls00  44051  rr-groth  44268  ismnushort  44270  rr-grothshortbi  44272  2sbc5g  44385  pm14.12  44390  2sb5nd  44531  uun2221  44784  uun2221p1  44785  uun2221p2  44786  2sb5ndVD  44881  2sb5ndALT  44903  iindif2f  45065  disjinfi  45099  climuz  45665  dfxlim2  45769  cncfshift  45795  dvnmul  45864  dvnprodlem2  45868  ismbl3  45907  ismbl4  45914  stoweidlem26  45947  stoweidlem35  45956  fourierdlem54  46081  fourierdlem83  46110  fourierdlem100  46127  fourierdlem104  46131  fourierdlem109  46136  fourierdlem112  46139  smfpimcc  46729  fcoresf1ob  46988  f1cof1b  46992  f1ocof1ob  46996  2reu8i  47028  dfdfat2  47043  ffnaov  47114  an4com24  47183  4an21  47185  iccpartiltu  47296  prproropf1olem0  47376  dfgric2  47768  2zrngmmgm  47975  rngcinvALTV  47999  ringcinvALTV  48033  opeliun2xp  48057  pgrpgt2nabl  48091  islindeps  48182  lindslinindsimp1  48186  lindslinindsimp2  48192  ldepslinc  48238  blen1b  48322  i0oii  48599  io1ii  48600  iscnrm3lem3  48615  isthinc2  48689  isthinc3  48690  isthincd2  48705  dffun3f  48774  setrec1lem3  48781  elpglem3  48805  elpg  48806