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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anbi1ci  626  anbi12i  627  bianass  639  an42  654  anandir  674  dfbi3  1047  dn1  1055  dfifp3  1063  ifpdfbi  1068  an3andi  1481  an33rean  1482  an33reanOLD  1483  anxordi  1525  cadcoma  1612  nic-mpALT  1673  nic-axALT  1675  3exdistr  1963  4exdistr  1964  19.27v  1992  19.27  2219  19.41  2227  2sb5  2271  dfsb7  2275  dfeumo  2535  mo4f  2565  eu3v  2568  eu6  2572  dfeu  2593  eu2  2609  eu4  2615  2mos  2649  2eu4  2654  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  reu2  3671  reu6  3672  reu4  3677  reu7  3678  rmo3f  3680  rmo4f  3681  2reu5lem3  3703  2reu5  3704  sbcimdv  3801  sbcg  3806  rmo3  3833  reuan  3840  dfpss2  4033  difdif  4078  raldifb  4092  inass  4167  dfss4  4206  dfin2  4208  indi  4221  indifdi  4231  indifdirOLD  4233  undif3  4238  difin0ss  4316  inssdif0  4317  2nreu  4389  2reu4lem  4471  rexdifpr  4607  reuprg0  4651  ssdifsn  4736  ssunpr  4780  uniprg  4870  uniprOLD  4872  uniun  4879  uniin  4880  csbuni  4885  dfiun2g  4978  iunin2  5019  iundif2  5022  iindif2  5025  iinin2  5026  elpwpw  5050  axrep1  5231  axrep4  5235  reusv2lem4  5345  eqvinop  5432  opcom  5446  fconstmpt  5681  opeliunxp  5686  xpundi  5687  elvvv  5694  opelinxp  5698  xpiindi  5778  elcnv2  5820  cnvuni  5829  dmuni  5857  brres  5931  dmres  5946  elidinxp  5984  restidsing  5993  elima3  6007  asymref  6057  imainss  6093  difxp  6103  xpdifid  6107  mptpreima  6177  coundir  6187  resco  6189  coass  6204  relrelss  6212  opreu2reurex  6233  dfpo2  6235  frpoind  6282  wfiOLD  6291  ordtri3or  6335  dffun2  6490  dffun2OLD  6491  dffun2OLDOLD  6492  dffun6  6493  dffun3  6494  dffun3OLD  6495  dffun4  6496  dffun5  6497  dffun6f  6498  dffun7  6512  dffun8  6513  dffun9  6514  svrelfun  6557  fncnv  6558  imadif  6569  dfmpt3  6619  fcnvres  6703  fint  6705  fin  6706  dff12  6721  fores  6750  dff1o4  6776  eqfnfv3  6968  fndmin  6979  fniniseg  6994  unpreima  6997  ffnfvf  7050  fsn2  7065  tpres  7133  fconstfv  7145  dff13f  7186  dff14a  7200  dff14b  7201  isocnv2  7259  f1opr  7394  eloprabga  7445  ffnov  7464  eqfnov  7466  foov  7509  uniuni  7675  tfindsg  7776  findsg  7815  funcnvuni  7847  opabex3d  7877  opabex3rd  7878  opabex3  7879  1stconst  8009  2ndconst  8010  frxp  8035  soxp  8038  suppvalbr  8052  suppofssd  8090  suppcoss  8094  mpoxopovel  8107  brtpos  8122  tpostpos  8133  dfsmo2  8249  dfrecs3  8274  dfrecs3OLD  8275  rdglem1  8317  tz7.49  8347  brwitnlem  8409  oeeu  8506  erinxp  8652  mapsncnv  8753  cbvixp  8774  ixpin  8783  ixpiin  8784  mptelixpg  8795  elixpsn  8797  ixpsnf1o  8798  xpassen  8932  omxpenlem  8939  sbthcl  8961  sbthfilem  9067  wemapsolem  9408  dford2  9478  inf2  9481  zfinf  9497  ttrclselem2  9584  trcl  9586  frind  9608  frr3g  9614  iscard2  9834  leweon  9869  aceq1  9975  dfac3  9979  dfac4  9980  dfac5lem2  9982  dfac5  9986  kmlem3  10010  kmlem4  10011  kmlem14  10021  kmlem15  10022  dfackm  10024  infmap2  10076  fin23lem25  10182  zorn2lem7  10360  brdom6disj  10390  zfcndrep  10472  zfcndinf  10476  fpwwe  10504  axgroth4  10690  grothprim  10692  grothtsk  10693  nqpr  10872  addsrmo  10931  mulsrmo  10932  opelreal  10988  elnnz  12431  elznn0nn  12435  peano2uz2  12510  nnwos  12757  dflt2  12984  xmullem  13100  4fvwrd4  13478  preduz  13480  elfznelfzo  13594  fzind2  13607  fsuppmapnn0fiubex  13814  hashinfxadd  14201  hashgt23el  14240  hashfun  14253  fi1uzind  14312  brfi1uzind  14313  opfi1uzind  14316  cotr2g  14787  shftdm  14882  rexfiuz  15159  cbvsum  15507  mertenslem2  15697  mertens  15698  cbvprod  15725  prodmo  15746  iprodmul  15813  divalglem10  16211  ndvdssub  16218  bitsmod  16243  algcvgblem  16380  isprm2  16485  isprm4  16487  hashdvds  16574  infpn2  16712  hashbc0  16804  xpscf  17374  funcpropd  17714  isffth2  17730  eldmcoa  17878  setcinv  17903  xpccatid  18003  yonedainv  18097  ispos  18130  ispos2  18131  joinfval2  18190  meetfval2  18204  istsr2  18400  isnsg2  18881  isnsg4  18892  isgim  18975  oppgid  19060  oppgcntz  19068  symgfix2  19121  efgval2  19426  iscyg2  19578  dmdprdd  19698  subgdmdprd  19733  issrg  19839  oppr1  19972  opprunit  19999  opprirred  20040  isrhm  20061  subsubrg2  20157  islmim  20431  lbsextg  20531  lidlnz  20606  isdomn2  20677  resubdrg  20920  unocv  20992  pjfval2  21023  islinds2  21127  opsrtoslem1  21369  mdetunilem8  21875  istop2g  22152  isbasis2g  22205  tgval2  22213  isclo2  22346  isnrm2  22616  is1stc2  22700  llyi  22732  isfbas2  23093  elfg  23129  ufinffr  23187  isfcls  23267  alexsubALTlem2  23306  alexsubALTlem3  23307  cnextcn  23325  ustfilxp  23471  iscusp2  23561  metustid  23817  isclmp  24367  iscvsp  24398  tcphcph  24508  iscau3  24549  caucfil  24554  mdegleb  25336  ellogdm  25901  dvdsflsumcom  26444  logfac2  26472  dchrelbas3  26493  dchrvmasumlema  26755  nosupno  26958  noinfno  26973  noinfbnd1lem1  26978  dmscut  27057  legtrid  27242  outpasch  27406  axcontlem5  27626  axcontlem6  27627  axcontlem7  27628  nb3grpr2  28040  iscplgr  28072  pthdlem1  28423  wwlksnextinj  28553  usgr2wspthon  28619  rusgrnumwwlkl1  28622  isclwwlk  28637  clwwlkccatlem  28642  clwwlknon2x  28756  iseupthf1o  28855  frcond3  28922  frgr3v  28928  4cycl2vnunb  28943  frgrncvvdeqlem2  28953  fusgr2wsp2nb  28987  numclwlk1lem1  29022  hhcms  29854  isch3  29892  ocsh  29934  pjhtheu  30045  pjpreeq  30049  h1deoi  30200  h1dei  30201  eleigvec  30608  cvbr2  30934  cvnbtwn2  30938  cvnbtwn4  30940  mdsl2i  30973  cvmdi  30975  mdsymlem6  31059  cdj3lem3b  31091  mo5f  31126  nmo  31127  rexunirn  31129  dmrab  31133  difrab2  31134  disjunsn  31220  unipreima  31268  dfcnv2  31300  1stpreima  31326  lsmsnorb2  31877  prmidl0  31923  ssmxidl  31939  zarcls  32122  rhmpreimacnlem  32132  isrnsiga  32379  rossros  32446  omsmeas  32590  eulerpartlemr  32641  eulerpartlemgvv  32643  ballotlemodife  32764  plymulx  32827  signstfvneq0  32851  bnj251  32981  bnj252  32982  bnj257  32986  bnj290  32989  bnj1304  33098  bnj153  33159  bnj543  33172  bnj571  33185  bnj580  33192  bnj607  33195  bnj882  33205  bnj964  33222  bnj996  33235  bnj1033  33248  bnj1176  33284  bnj1186  33286  bnj1189  33288  bnj1204  33291  bnj1253  33296  bnj1452  33331  bnj1463  33334  dff15  33355  fineqvrep  33363  fineqvac  33365  lfuhgr3  33380  cusgredgex2  33383  usgrgt2cycl  33391  2cycl2d  33400  dfacycgr1  33405  erdszelem9  33460  cvmlift2lem9  33572  cvmlift2lem13  33576  satfvsucsuc  33626  satfdm  33630  satf0  33633  fmlasucdisj  33660  satffunlem  33662  satffunlem1lem1  33663  satffunlem2lem1  33665  elmthm  33837  axinfprim  33946  axacprim  33947  xpab  33967  dfso2  34013  dford5reg  34043  dfon2lem5  34048  dfon2  34053  xpord3lem  34079  naddasslem2  34133  made0  34167  brtxp2  34322  brpprod3a  34327  dfom5b  34353  brcart  34373  brimg  34378  funpartlem  34383  dfrecs2  34391  cgrxfr  34496  segletr  34555  trer  34644  fneval  34680  neifg  34699  df3nandALT1  34727  andnand1  34729  nandsym1  34750  bj-eu3f  35163  bj-csbsnlem  35226  bj-snsetex  35290  bj-elsngl  35295  bj-snglc  35296  bj-restuni  35424  bj-dfmpoa  35445  bj-imdirco  35517  mptsnunlem  35665  icorempo  35678  isbasisrelowllem2  35683  relowlpssretop  35691  rdgeqoa  35697  difunieq  35701  dffinxpf  35712  nlpineqsn  35735  curf  35911  finixpnum  35918  ptrest  35932  poimirlem1  35934  poimirlem14  35947  poimirlem16  35949  poimirlem19  35952  poimirlem25  35958  poimirlem26  35959  poimirlem27  35960  poimir  35966  cnambfre  35981  itg2addnc  35987  ftc1anc  36014  opropabco  36038  isdrngo1  36270  keridl  36346  ispridlc  36384  selconj  36414  eldmqsres  36603  cnvepres  36615  ecinn0  36670  alrmomorn  36675  moantr  36681  dfxrn2  36694  disjressuc2  36706  inxpxrn  36713  rnxrnres  36717  coss2cnvepres  36736  refrelredund4  36953  dferALTV2  36986  dfeldisj3  37037  dfpart2  37087  prtlem70  37175  prtlem100  37177  prtlem15  37193  islshpat  37335  lcvbr2  37340  lcvbr3  37341  lcvnbtwn2  37345  ellkr  37407  cvrval2  37592  cvrnbtwn2  37593  cvrnbtwn3  37594  cvrnbtwn4  37597  ishlat2  37671  lplnexatN  37882  islvol5  37898  dath  38055  pclfinclN  38269  lhpexle3  38331  4atex2  38396  4atex2-0bOLDN  38398  isltrn2N  38439  cdleme0nex  38609  cdleme22b  38660  cdlemg17pq  38991  cdlemg19  39003  cdlemg21  39005  cdlemg33d  39028  dibopelvalN  39462  dibopelval2  39464  dib1dim  39484  dicelval2N  39501  diclspsn  39513  lcdlss  39938  mapd1o  39967  3factsumint2  40335  3factsumint3  40336  3factsumint  40338  sticksstones16  40426  sticksstones21  40431  metakunt1  40433  mhphf  40596  mzpcompact2lem  40886  fz1eqin  40904  rexrabdioph  40929  expdiophlem1  41157  dford4  41165  fnwe2lem2  41190  fgraphopab  41349  faosnf0.11b  41408  ifpidg  41472  rp-fakeinunass  41496  rp-isfinite6  41499  dfsucon  41504  elinintrab  41558  elnonrel  41566  elmapintab  41577  dfrtrcl5  41610  imaiun1  41632  coiun1  41633  rfovcnvf1od  41985  andi3or  42005  uneqsn  42006  ntrneicls00  42072  rr-groth  42290  ismnushort  42292  rr-grothshortbi  42294  2sbc5g  42407  pm14.12  42412  2sb5nd  42553  uun2221  42806  uun2221p1  42807  uun2221p2  42808  2sb5ndVD  42903  2sb5ndALT  42925  disjinfi  43110  climuz  43673  dfxlim2  43777  cncfshift  43803  dvnmul  43872  dvnprodlem2  43876  ismbl3  43915  ismbl4  43922  stoweidlem26  43955  stoweidlem35  43964  fourierdlem54  44089  fourierdlem83  44118  fourierdlem100  44135  fourierdlem104  44139  fourierdlem109  44144  fourierdlem112  44147  smfpimcc  44735  fcoresf1ob  44985  f1cof1b  44987  f1ocof1ob  44991  2reu8i  45023  dfdfat2  45038  ffnaov  45109  an4com24  45178  4an21  45180  iccpartiltu  45292  prproropf1olem0  45372  isrnghm  45868  2zrngmmgm  45922  rngcinv  45957  rngcinvALTV  45969  ringcinv  46008  ringcinvALTV  46032  opeliun2xp  46086  pgrpgt2nabl  46120  islindeps  46212  lindslinindsimp1  46216  lindslinindsimp2  46222  ldepslinc  46268  blen1b  46352  i0oii  46631  io1ii  46632  iscnrm3lem3  46647  isthinc2  46721  isthinc3  46722  isthincd2  46737  dffun3f  46806  setrec1lem3  46813  elpglem3  46836  elpg  46837