Theorem anbi2i 635

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi1ci  638  anbi12i  640  bianass  655  an42  670  anandir  690  dfbi3  1065  dn1  1073  dfifp3  1081  ifpdfbiOLD  1087  4anpull2OLD  1383  an3andi  1513  an33rean  1514  anxordi  1556  cadcoma  1645  nic-mpALT  1705  nic-axALT  1707  3exdistr  1993  4exdistr  1994  19.27v  2028  19.27  2266  19.41  2274  2sb5  2316  dfsb7  2317  dfeumo  2567  mo4f  2598  eu3v  2601  eu6  2605  dfeu  2626  eu2  2640  eu4  2646  2mos  2680  2eu4  2685  r3ex  3207  ceqsex3v  3510  ceqsex4v  3511  ceqsex8v  3513  reu2  3691  reu6  3692  reu4  3697  reu7  3698  rmo3f  3700  rmo4f  3701  2reu5lem3  3723  2reu5  3724  sbcimdv  3815  sbcg  3819  rmo3  3845  reuan  3853  dfpss2  4045  difdif  4092  raldifb  4106  inass  4183  dfss4  4225  dfin2  4227  indi  4240  indifdi  4250  undif3  4256  difin0ss  4331  inssdif0OLD  4333  2nreu  4412  2reu4lem  4487  rexdifpr  4628  reuprg0  4671  ssdifsn  4759  ssunpr  4802  uniprg  4891  uniun  4898  uniinOLD  4900  csbuni  4906  dfiun2g  4997  iunin2  5038  iundif2  5041  iindif2  5046  iinin2  5047  elpwpw  5071  axrep1  5242  axrep4v  5246  axrep4  5247  axrep4OLD  5248  reusv2lem4  5375  eqvinop  5472  opcom  5487  fconstmpt  5726  opeliunxp  5731  opeliun2xp  5732  xpundi  5733  elvvv  5740  opelinxp  5744  xpiindi  5824  elcnv2  5866  cnvuni  5879  dmuni  5907  brres  5988  dmres  6014  elidinxp  6049  restidsing  6058  elima3  6072  asymref  6119  imainss  6154  difxp  6164  xpdifid  6168  xpdifcnvepel  6169  mptpreima  6242  coundir  6252  resco  6254  coass  6270  relrelss  6278  opreu2reurex  6299  dfpo2  6301  frpoind  6347  ordtri3or  6397  dffun2  6550  dffun6  6551  dffun3  6552  dffun4  6553  dffun5  6554  dffun6f  6555  dffun7  6567  dffun8  6568  dffun9  6569  svrelfun  6612  fncnv  6613  imadif  6624  dfmpt3  6673  fcnvres  6759  fint  6761  fin  6762  dff12  6777  fores  6806  dff1o4  6833  eqfnfv3  7031  fndmin  7044  fniniseg  7059  unpreima  7062  ffnfvf  7119  fsn2  7136  tpres  7203  fconstfv  7214  dff13f  7257  dff14a  7272  dff14b  7273  isocnv2  7333  f1opr  7472  eloprabga  7525  ffnov  7542  eqfnov  7545  foov  7590  uniuni  7763  tfindsg  7859  findsg  7896  funcnvuni  7931  opabex3d  7964  opabex3rd  7965  opabex3  7966  1stconst  8097  2ndconst  8098  frxp  8124  soxp  8127  xpord3lem  8147  suppvalbr  8162  suppofssd  8201  suppcoss  8205  mpoxopovel  8218  brtpos  8233  tpostpos  8244  dfsmo2  8336  dfrecs3  8361  rdglem1  8404  tz7.49  8434  brwitnlem  8494  oeeu  8591  naddasslem2  8684  brinxper  8726  erinxp  8791  mapsncnv  8893  cbvixp  8914  cbvixpv  8915  ixpin  8923  ixpiin  8924  mptelixpg  8935  elixpsn  8937  ixpsnf1o  8938  xpassen  9061  omxpenlem  9068  sbthcl  9089  sbthfilem  9184  wemapsolem  9514  dford2  9591  inf2  9594  zfinf  9610  ttrclselem2  9697  trcl  9699  frind  9724  frr3g  9730  iscard2  9973  leweon  10006  aceq1  10112  dfac3  10116  dfac4  10117  dfac5lem2  10119  dfac5  10123  kmlem3  10147  kmlem4  10148  kmlem14  10158  kmlem15  10159  dfackm  10161  infmap2  10211  fin23lem25  10318  zorn2lem7  10496  brdom6disj  10526  zfcndrep  10609  zfcndinf  10613  fpwwe  10641  axgroth4  10827  grothprim  10829  grothtsk  10830  nqpr  11009  addsrmo  11068  mulsrmo  11069  opelreal  11125  elnnz  12611  elznn0nn  12615  peano2uz2  12694  nnwos  12949  dflt2  13183  xmullem  13300  4fvwrd4  13687  preduz  13689  elfznelfzo  13813  fzind2  13828  fsuppmapnn0fiubex  14039  hashinfxadd  14432  hashgt23el  14472  hashfun  14485  fi1uzind  14555  brfi1uzind  14556  opfi1uzind  14559  cotr2g  15024  shftdm  15119  rexfiuz  15410  cbvsum  15757  cbvsumv  15758  mertenslem2  15950  mertens  15951  cbvprod  15978  cbvprodv  15979  prodeq1i  15981  prodmo  16001  iprodmul  16068  divalglem10  16470  ndvdssub  16477  bitsmod  16504  algcvgblem  16645  isprm2  16750  isprm4  16752  hashdvds  16844  infpn2  16983  hashbc0  17075  xpscf  17629  funcpropd  17969  isffth2  17985  eldmcoa  18132  setcinv  18157  xpccatid  18254  yonedainv  18347  ispos  18380  ispos2  18381  joinfval2  18438  meetfval2  18452  istsr2  18650  isnsg2  19232  isnsg4  19243  isgim  19342  oppgid  19436  oppgcntz  19444  symgfix2  19496  efgval2  19804  iscyg2  19962  dmdprdd  20081  subgdmdprd  20116  issrg  20280  oppr1  20443  opprunit  20470  opprirred  20515  isrnghm  20534  isrhm  20572  issubrng  20661  subsubrng2  20678  subsubrg2  20713  rngcinv  20751  ringcinv  20785  isdomn2  20825  islmim  21198  lbsextg  21301  lidlnz  21391  prmidl0  21493  resubdrg  21773  unocv  21845  pjfval2  21874  islinds2  21978  opsrtoslem1  22221  mdetunilem8  22791  istop2g  23068  isbasis2g  23120  tgval2  23128  isclo2  23260  isnrm2  23530  is1stc2  23614  llyi  23646  isfbas2  24007  elfg  24043  ufinffr  24101  isfcls  24181  alexsubALTlem2  24220  alexsubALTlem3  24221  cnextcn  24239  ustfilxp  24385  iscusp2  24473  metustid  24726  isclmp  25271  iscvsp  25302  tcphcph  25411  iscau3  25452  caucfil  25457  mdegleb  26236  plymulidp  26458  ellogdm  26819  dvdsflsumcom  27367  logfac2  27396  dchrelbas3  27417  dchrvmasumlema  27679  nosupno  27882  noinfno  27897  noinfbnd1lem1  27902  dmcuts  27999  made0  28071  mulsproplem5  28328  norecdiv  28398  elnnzs  28609  uzsind  28613  zsoring  28617  legtrid  28875  outpasch  29052  tgaltai  29232  axcontlem5  29333  axcontlem6  29334  axcontlem7  29335  nb3grpr2  29748  iscplgr  29780  dfpth2  30093  pthdlem1  30130  wwlksnextinj  30263  usgr2wspthon  30332  rusgrnumwwlkl1  30335  isclwwlk  30350  clwwlkccatlem  30355  clwwlknon2x  30469  iseupthf1o  30568  frcond3  30635  frgr3v  30641  4cycl2vnunb  30656  frgrncvvdeqlem2  30666  fusgr2wsp2nb  30700  numclwlk1lem1  30735  hhcms  31570  isch3  31608  ocsh  31650  pjhtheu  31761  pjpreeq  31765  h1deoi  31916  h1dei  31917  eleigvec  32324  cvbr2  32650  cvnbtwn2  32654  cvnbtwn4  32656  mdsl2i  32689  cvmdi  32691  mdsymlem6  32775  cdj3lem3b  32807  mo5f  32850  nmo  32851  rexunirn  32853  dmrab  32858  difrab2  32859  disjunsn  32954  unipreima  33003  dfcnv2  33035  1stpreima  33067  isunit2  33572  lsmsnorb2  33718  ssmxidl  33770  1arithufdlem4  33850  ressply1mon1p  33871  extdgfialglem1  34095  zarcls  34277  rhmpreimacnlem  34287  isrnsiga  34516  rossros  34583  omsmeas  34726  eulerpartlemr  34777  eulerpartlemgvv  34779  ballotlemodife  34901  signstfvneq0  34972  bnj251  35104  bnj252  35105  bnj257  35109  bnj290  35112  bnj1304  35220  bnj153  35281  bnj543  35294  bnj571  35307  bnj580  35314  bnj607  35317  bnj882  35327  bnj964  35344  bnj996  35357  bnj1033  35370  bnj1176  35406  bnj1186  35408  bnj1189  35410  bnj1204  35413  bnj1253  35418  bnj1452  35453  bnj1463  35456  dff15  35485  axprALT2  35516  fineqvrep  35539  fineqvac  35541  kardexen  35588  lfuhgr3  35624  cusgredgex2  35627  usgrgt2cycl  35634  2cycl2d  35643  dfacycgr1  35648  erdszelem9  35703  cvmlift2lem9  35815  cvmlift2lem13  35819  satfvsucsuc  35869  satfdm  35873  satf0  35876  fmlasucdisj  35903  satffunlem  35905  satffunlem1lem1  35906  satffunlem2lem1  35908  elmthm  36080  axinfprim  36210  axacprim  36211  xpab  36230  dfso2  36259  dford5reg  36284  dfon2lem5  36289  dfon2  36294  brtxp2  36383  brpprod3a  36388  dfom5b  36414  brcart  36434  brimg  36439  funpartlem  36446  dfrecs2  36454  cgrxfr  36559  segletr  36618  sumeq2si  36746  prodeq2si  36748  cbvprodvw2  36791  trer  36859  fneval  36895  neifg  36914  df3nandALT1  36942  andnand1  36944  nandsym1  36965  weiunlem  37006  regsfromregtco  37081  mh-infprim2bi  37090  mh-infprim3bi  37091  bj-df-sb  37304  bj-dfsbc  37306  bj-eu3f  37508  bj-csbsnlem  37570  bj-snsetex  37631  bj-elsngl  37636  bj-snglc  37637  bj-restuni  37771  bj-dfmpoa  37792  bj-imdirco  37866  mptsnunlem  38016  icorempo  38029  isbasisrelowllem2  38034  relowlpssretop  38042  rdgeqoa  38048  difunieq  38052  dffinxpf  38063  nlpineqsn  38086  curf  38281  finixpnum  38288  ptrest  38302  poimirlem1  38304  poimirlem14  38317  poimirlem16  38319  poimirlem19  38322  poimirlem25  38328  poimirlem26  38329  poimirlem27  38330  poimir  38336  cnambfre  38351  itg2addnc  38357  ftc1anc  38384  opropabco  38407  isdrngo1  38639  keridl  38715  ispridlc  38753  selconj  38781  eldmres3  38964  eldmqsres  38974  cnvepres  38985  ecinn0  39034  alrmomorn  39039  moantr  39053  dfxrn2  39066  disjressuc2  39092  inxpxrn  39099  rnxrnres  39103  coss2cnvepres  39189  refrelredund4  39400  dferALTV2  39434  dfeldisj3  39492  dfpart2  39553  dfpeters2  39655  petseq  39657  prtlem70  39663  prtlem100  39665  prtlem15  39681  islshpat  39823  lcvbr2  39828  lcvbr3  39829  lcvnbtwn2  39833  ellkr  39895  cvrval2  40080  cvrnbtwn2  40081  cvrnbtwn3  40082  cvrnbtwn4  40085  ishlat2  40159  lplnexatN  40369  islvol5  40385  dath  40542  pclfinclN  40756  lhpexle3  40818  4atex2  40883  4atex2-0bOLDN  40885  isltrn2N  40926  cdleme0nex  41096  cdleme22b  41147  cdlemg17pq  41478  cdlemg19  41490  cdlemg21  41492  cdlemg33d  41515  dibopelvalN  41949  dibopelval2  41951  dib1dim  41971  dicelval2N  41988  diclspsn  42000  lcdlss  42425  mapd1o  42454  3factsumint2  42821  3factsumint3  42822  3factsumint  42824  hashnexinj  42927  sticksstones16  42961  sticksstones21  42966  unitscyglem3  42996  supinf  43042  fimgmcyclem  43333  eu6w  43440  mzpcompact2lem  43514  fz1eqin  43532  rexrabdioph  43553  expdiophlem1  43780  dford4  43788  fnwe2lem2  43810  fgraphopab  43962  dflim6  44023  onsucf1olem  44029  onsucrn  44030  nnoeomeqom  44071  faosnf0.11b  44185  ifpidg  44249  rp-fakeinunass  44273  rp-isfinite6  44276  dfsucon  44281  elinintrab  44335  elnonrel  44343  elmapintab  44354  dfrtrcl5  44387  imaiun1  44409  coiun1  44410  rfovcnvf1od  44762  andi3or  44782  uneqsn  44783  ntrneicls00  44847  rr-groth  45041  ismnushort  45043  rr-grothshortbi  45045  2sbc5g  45158  pm14.12  45163  2sb5nd  45301  uun2221  45553  uun2221p1  45554  uun2221p2  45555  2sb5ndVD  45650  2sb5ndALT  45672  modelaxreplem3  45721  iindif2f  45910  disjinfi  45942  climuz  46490  dfxlim2  46594  cncfshift  46620  dvnmul  46689  dvnprodlem2  46693  ismbl3  46732  ismbl4  46739  stoweidlem26  46772  stoweidlem35  46781  fourierdlem54  46906  fourierdlem83  46935  fourierdlem100  46952  fourierdlem104  46956  fourierdlem109  46961  fourierdlem112  46964  smfpimcc  47554  fcoresf1ob  47842  f1cof1b  47846  f1ocof1ob  47850  2reu8i  47882  dfdfat2  47897  ffnaov  47968  an4com24  48037  4an21  48039  iccpartiltu  48203  prproropf1olem0  48283  dfgric2  48712  gpgvtxedg0  48860  gpgvtxedg1  48861  gpgprismgr4cycllem10  48901  grlimedgnedg  48928  2zrngmmgm  49049  rngcinvALTV  49073  ringcinvALTV  49107  isprmrng  49133  pgrpgt2nabl  49178  islindeps  49265  lindslinindsimp1  49269  lindslinindsimp2  49275  ldepslinc  49321  blen1b  49400  coxp  49643  i0oii  49730  io1ii  49731  isthinc2  50230  isthinc3  50231  isthincd2  50247  istermc2  50285  istermc3  50286  dffun3f  50492  setrec1lem3  50499  elpglem3  50523  elpg  50524  alsanmo  50620  ralsanmo  50621  2alsraln0  50627  2alsraln0id  50628