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  1995  19.27  2228  19.41  2236  2sb5  2278  dfsb7  2279  dfeumo  2530  mo4f  2560  eu3v  2563  eu6  2567  dfeu  2588  eu2  2602  eu4  2608  2mos  2642  2mosOLD  2643  2eu4  2648  r3ex  3176  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  reu2  3696  reu6  3697  reu4  3702  reu7  3703  rmo3f  3705  rmo4f  3706  2reu5lem3  3728  2reu5  3729  sbcimdv  3822  sbcg  3826  rmo3  3852  reuan  3859  dfpss2  4051  difdif  4098  raldifb  4112  inass  4191  dfss4  4232  dfin2  4234  indi  4247  indifdi  4257  undif3  4263  difin0ss  4336  inssdif0  4337  2nreu  4407  2reu4lem  4485  rexdifpr  4623  reuprg0  4666  ssdifsn  4752  ssunpr  4798  uniprg  4887  uniun  4894  uniin  4895  csbuni  4900  dfiun2g  4994  iunin2  5035  iundif2  5038  iindif2  5041  iinin2  5042  elpwpw  5066  axrep1  5235  axrep4v  5239  axrep4  5240  axrep4OLD  5241  reusv2lem4  5356  eqvinop  5447  opcom  5461  fconstmpt  5700  opeliunxp  5705  opeliun2xp  5706  xpundi  5707  elvvv  5714  opelinxp  5718  xpiindi  5799  elcnv2  5841  cnvuni  5850  dmuni  5878  brres  5957  dmres  5983  elidinxp  6015  restidsing  6024  elima3  6038  asymref  6089  imainss  6127  difxp  6137  xpdifid  6141  mptpreima  6211  coundir  6221  resco  6223  coass  6238  relrelss  6246  opreu2reurex  6267  dfpo2  6269  frpoind  6315  ordtri3or  6364  dffun2  6521  dffun2OLD  6522  dffun2OLDOLD  6523  dffun6  6524  dffun3  6525  dffun3OLD  6526  dffun4  6527  dffun5  6528  dffun6f  6529  dffun7  6543  dffun8  6544  dffun9  6545  svrelfun  6588  fncnv  6589  imadif  6600  dfmpt3  6652  fcnvres  6737  fint  6739  fin  6740  dff12  6755  fores  6782  dff1o4  6808  eqfnfv3  7005  fndmin  7017  fniniseg  7032  unpreima  7035  ffnfvf  7092  fsn2  7108  tpres  7175  fconstfv  7186  dff13f  7230  dff14a  7245  dff14b  7246  isocnv2  7306  f1opr  7445  eloprabga  7498  ffnov  7515  eqfnov  7518  foov  7563  uniuni  7738  tfindsg  7837  findsg  7873  funcnvuni  7908  opabex3d  7944  opabex3rd  7945  opabex3  7946  1stconst  8079  2ndconst  8080  frxp  8105  soxp  8108  xpord3lem  8128  suppvalbr  8143  suppofssd  8182  suppcoss  8186  mpoxopovel  8199  brtpos  8214  tpostpos  8225  dfsmo2  8316  dfrecs3  8341  rdglem1  8383  tz7.49  8413  brwitnlem  8471  oeeu  8567  naddasslem2  8659  brinxper  8700  erinxp  8764  mapsncnv  8866  cbvixp  8887  cbvixpv  8888  ixpin  8896  ixpiin  8897  mptelixpg  8908  elixpsn  8910  ixpsnf1o  8911  xpassen  9035  omxpenlem  9042  sbthcl  9063  sbthfilem  9162  wemapsolem  9503  dford2  9573  inf2  9576  zfinf  9592  ttrclselem2  9679  trcl  9681  frind  9703  frr3g  9709  iscard2  9929  leweon  9964  aceq1  10070  dfac3  10074  dfac4  10075  dfac5lem2  10077  dfac5  10082  kmlem3  10106  kmlem4  10107  kmlem14  10117  kmlem15  10118  dfackm  10120  infmap2  10170  fin23lem25  10277  zorn2lem7  10455  brdom6disj  10485  zfcndrep  10567  zfcndinf  10571  fpwwe  10599  axgroth4  10785  grothprim  10787  grothtsk  10788  nqpr  10967  addsrmo  11026  mulsrmo  11027  opelreal  11083  elnnz  12539  elznn0nn  12543  peano2uz2  12622  nnwos  12874  dflt2  13108  xmullem  13224  4fvwrd4  13609  preduz  13611  elfznelfzo  13733  fzind2  13746  fsuppmapnn0fiubex  13957  hashinfxadd  14350  hashgt23el  14389  hashfun  14402  fi1uzind  14472  brfi1uzind  14473  opfi1uzind  14476  cotr2g  14942  shftdm  15037  rexfiuz  15314  cbvsum  15661  cbvsumv  15662  mertenslem2  15851  mertens  15852  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  prodmo  15902  iprodmul  15969  divalglem10  16372  ndvdssub  16379  bitsmod  16406  algcvgblem  16547  isprm2  16652  isprm4  16654  hashdvds  16745  infpn2  16884  hashbc0  16976  xpscf  17528  funcpropd  17864  isffth2  17880  eldmcoa  18027  setcinv  18052  xpccatid  18149  yonedainv  18242  ispos  18275  ispos2  18276  joinfval2  18333  meetfval2  18347  istsr2  18543  isnsg2  19088  isnsg4  19099  isgim  19194  oppgid  19288  oppgcntz  19296  symgfix2  19346  efgval2  19654  iscyg2  19812  dmdprdd  19931  subgdmdprd  19966  issrg  20097  oppr1  20259  opprunit  20286  opprirred  20331  isrnghm  20350  isrhm  20387  issubrng  20456  subsubrng2  20473  subsubrg2  20508  rngcinv  20546  ringcinv  20580  isdomn2  20620  isdomn2OLD  20621  islmim  20969  lbsextg  21072  lidlnz  21152  resubdrg  21517  unocv  21589  pjfval2  21618  islinds2  21722  opsrtoslem1  21962  mdetunilem8  22506  istop2g  22783  isbasis2g  22835  tgval2  22843  isclo2  22975  isnrm2  23245  is1stc2  23329  llyi  23361  isfbas2  23722  elfg  23758  ufinffr  23816  isfcls  23896  alexsubALTlem2  23935  alexsubALTlem3  23936  cnextcn  23954  ustfilxp  24100  iscusp2  24189  metustid  24442  isclmp  24997  iscvsp  25028  tcphcph  25137  iscau3  25178  caucfil  25183  mdegleb  25969  ellogdm  26548  dvdsflsumcom  27098  logfac2  27128  dchrelbas3  27149  dchrvmasumlema  27411  nosupno  27615  noinfno  27630  noinfbnd1lem1  27635  dmscut  27723  made0  27785  mulsproplem5  28023  norecdiv  28093  elnnzs  28289  uzsind  28293  legtrid  28518  outpasch  28682  axcontlem5  28895  axcontlem6  28896  axcontlem7  28897  nb3grpr2  29310  iscplgr  29342  dfpth2  29659  pthdlem1  29696  wwlksnextinj  29829  usgr2wspthon  29895  rusgrnumwwlkl1  29898  isclwwlk  29913  clwwlkccatlem  29918  clwwlknon2x  30032  iseupthf1o  30131  frcond3  30198  frgr3v  30204  4cycl2vnunb  30219  frgrncvvdeqlem2  30229  fusgr2wsp2nb  30263  numclwlk1lem1  30298  hhcms  31132  isch3  31170  ocsh  31212  pjhtheu  31323  pjpreeq  31327  h1deoi  31478  h1dei  31479  eleigvec  31886  cvbr2  32212  cvnbtwn2  32216  cvnbtwn4  32218  mdsl2i  32251  cvmdi  32253  mdsymlem6  32337  cdj3lem3b  32369  mo5f  32418  nmo  32419  rexunirn  32421  dmrab  32426  difrab2  32427  disjunsn  32523  unipreima  32567  dfcnv2  32600  1stpreima  32630  isunit2  33191  lsmsnorb2  33363  prmidl0  33421  ssmxidl  33445  1arithufdlem4  33518  ressply1mon1p  33537  zarcls  33864  rhmpreimacnlem  33874  isrnsiga  34103  rossros  34170  omsmeas  34314  eulerpartlemr  34365  eulerpartlemgvv  34367  ballotlemodife  34489  plymulx  34539  signstfvneq0  34563  bnj251  34692  bnj252  34693  bnj257  34697  bnj290  34700  bnj1304  34809  bnj153  34870  bnj543  34883  bnj571  34896  bnj580  34903  bnj607  34906  bnj882  34916  bnj964  34933  bnj996  34946  bnj1033  34959  bnj1176  34995  bnj1186  34997  bnj1189  34999  bnj1204  35002  bnj1253  35007  bnj1452  35042  bnj1463  35045  dff15  35074  fineqvrep  35085  fineqvac  35087  lfuhgr3  35107  cusgredgex2  35110  usgrgt2cycl  35117  2cycl2d  35126  dfacycgr1  35131  erdszelem9  35186  cvmlift2lem9  35298  cvmlift2lem13  35302  satfvsucsuc  35352  satfdm  35356  satf0  35359  fmlasucdisj  35386  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  elmthm  35563  axinfprim  35693  axacprim  35694  xpab  35713  dfso2  35742  dford5reg  35770  dfon2lem5  35775  dfon2  35780  brtxp2  35869  brpprod3a  35874  dfom5b  35900  brcart  35920  brimg  35925  funpartlem  35930  dfrecs2  35938  cgrxfr  36043  segletr  36102  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  trer  36304  fneval  36340  neifg  36359  df3nandALT1  36387  andnand1  36389  nandsym1  36410  weiunlem2  36451  bj-eu3f  36829  bj-csbsnlem  36891  bj-snsetex  36951  bj-elsngl  36956  bj-snglc  36957  bj-restuni  37085  bj-dfmpoa  37106  bj-imdirco  37178  mptsnunlem  37326  icorempo  37339  isbasisrelowllem2  37344  relowlpssretop  37352  rdgeqoa  37358  difunieq  37362  dffinxpf  37373  nlpineqsn  37396  curf  37592  finixpnum  37599  ptrest  37613  poimirlem1  37615  poimirlem14  37628  poimirlem16  37630  poimirlem19  37633  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimir  37647  cnambfre  37662  itg2addnc  37668  ftc1anc  37695  opropabco  37718  isdrngo1  37950  keridl  38026  ispridlc  38064  selconj  38094  eldmres3  38265  eldmqsres  38275  cnvepres  38286  ecinn0  38335  alrmomorn  38340  moantr  38346  dfxrn2  38358  disjressuc2  38374  inxpxrn  38381  rnxrnres  38385  coss2cnvepres  38409  refrelredund4  38626  dferALTV2  38660  dfeldisj3  38711  dfpart2  38761  prtlem70  38850  prtlem100  38852  prtlem15  38868  islshpat  39010  lcvbr2  39015  lcvbr3  39016  lcvnbtwn2  39020  ellkr  39082  cvrval2  39267  cvrnbtwn2  39268  cvrnbtwn3  39269  cvrnbtwn4  39272  ishlat2  39346  lplnexatN  39557  islvol5  39573  dath  39730  pclfinclN  39944  lhpexle3  40006  4atex2  40071  4atex2-0bOLDN  40073  isltrn2N  40114  cdleme0nex  40284  cdleme22b  40335  cdlemg17pq  40666  cdlemg19  40678  cdlemg21  40680  cdlemg33d  40703  dibopelvalN  41137  dibopelval2  41139  dib1dim  41159  dicelval2N  41176  diclspsn  41188  lcdlss  41613  mapd1o  41642  3factsumint2  42010  3factsumint3  42011  3factsumint  42013  hashnexinj  42116  sticksstones16  42150  sticksstones21  42155  unitscyglem3  42185  supinf  42230  fimgmcyclem  42521  eu6w  42664  mzpcompact2lem  42739  fz1eqin  42757  rexrabdioph  42782  expdiophlem1  43010  dford4  43018  fnwe2lem2  43040  fgraphopab  43192  dflim6  43253  onsucf1olem  43259  onsucrn  43260  nnoeomeqom  43301  faosnf0.11b  43416  ifpidg  43480  rp-fakeinunass  43504  rp-isfinite6  43507  dfsucon  43512  elinintrab  43566  elnonrel  43574  elmapintab  43585  dfrtrcl5  43618  imaiun1  43640  coiun1  43641  rfovcnvf1od  43993  andi3or  44013  uneqsn  44014  ntrneicls00  44078  rr-groth  44288  ismnushort  44290  rr-grothshortbi  44292  2sbc5g  44405  pm14.12  44410  2sb5nd  44550  uun2221  44802  uun2221p1  44803  uun2221p2  44804  2sb5ndVD  44899  2sb5ndALT  44921  modelaxreplem3  44970  iindif2f  45154  disjinfi  45186  climuz  45742  dfxlim2  45846  cncfshift  45872  dvnmul  45941  dvnprodlem2  45945  ismbl3  45984  ismbl4  45991  stoweidlem26  46024  stoweidlem35  46033  fourierdlem54  46158  fourierdlem83  46187  fourierdlem100  46204  fourierdlem104  46208  fourierdlem109  46213  fourierdlem112  46216  smfpimcc  46806  fcoresf1ob  47074  f1cof1b  47078  f1ocof1ob  47082  2reu8i  47114  dfdfat2  47129  ffnaov  47200  an4com24  47269  4an21  47271  iccpartiltu  47423  prproropf1olem0  47503  dfgric2  47915  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgprismgr4cycllem10  48094  2zrngmmgm  48240  rngcinvALTV  48264  ringcinvALTV  48298  pgrpgt2nabl  48354  islindeps  48442  lindslinindsimp1  48446  lindslinindsimp2  48452  ldepslinc  48498  blen1b  48577  coxp  48821  i0oii  48908  io1ii  48909  isthinc2  49409  isthinc3  49410  isthincd2  49426  istermc2  49464  istermc3  49465  dffun3f  49671  setrec1lem3  49678  elpglem3  49702  elpg  49703