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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi1ci  625  anbi12i  626  bianass  638  an42  653  anandir  673  dfbi3  1046  dn1  1054  dfifp3  1062  ifpdfbi  1067  an3andi  1480  an33rean  1481  an33reanOLD  1482  anxordi  1520  norassOLD  1536  cadcoma  1615  nic-mpALT  1676  nic-axALT  1678  3exdistr  1965  4exdistr  1966  19.27v  1994  19.27  2223  19.41  2231  2sb5  2275  dfsb7  2279  dfeumo  2537  mo4f  2567  eu3v  2570  eu6  2574  dfeu  2595  eu2  2611  eu4  2617  2mos  2651  2eu4  2656  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  reu2  3655  reu6  3656  reu4  3661  reu7  3662  rmo3f  3664  rmo4f  3665  2reu5lem3  3687  2reu5  3688  sbcimdv  3786  sbcg  3791  rmo3  3818  reuan  3825  dfpss2  4016  difdif  4061  raldifb  4075  inass  4150  dfss4  4189  dfin2  4191  indi  4204  indifdi  4214  indifdirOLD  4216  undif3  4221  difin0ss  4299  inssdif0  4300  2nreu  4372  2reu4lem  4453  rexdifpr  4591  reuprg0  4635  ssdifsn  4718  ssunpr  4762  uniprg  4853  uniprOLD  4855  uniun  4861  uniin  4862  csbuni  4867  iunin2  4996  iundif2  4999  iindif2  5002  iinin2  5003  elpwpw  5027  axrep1  5206  axrep4  5210  reusv2lem4  5319  eqvinop  5395  opcom  5409  fconstmpt  5640  opeliunxp  5645  xpundi  5646  elvvv  5653  opelinxp  5657  xpiindi  5733  elcnv2  5775  cnvuni  5784  dmuni  5812  brres  5887  dmres  5902  elidinxp  5940  restidsing  5951  elima3  5965  asymref  6010  imainss  6046  difxp  6056  xpdifid  6060  mptpreima  6130  coundir  6141  resco  6143  coass  6158  relrelss  6165  opreu2reurex  6186  dfpo2  6188  frpoind  6230  wfiOLD  6239  ordtri3or  6283  dffun2  6428  dffun3  6429  dffun4  6430  dffun5  6431  dffun6f  6432  dffun7  6445  dffun8  6446  dffun9  6447  svrelfun  6490  fncnv  6491  imadif  6502  dfmpt3  6551  fcnvres  6635  fint  6637  fin  6638  dff12  6653  fores  6682  dff1o4  6708  eqfnfv3  6893  fndmin  6904  fniniseg  6919  unpreima  6922  ffnfvf  6975  fsn2  6990  tpres  7058  fconstfv  7070  dff13f  7110  dff14a  7124  dff14b  7125  isocnv2  7182  f1opr  7309  eloprabga  7360  ffnov  7379  eqfnov  7381  foov  7424  uniuni  7590  tfindsg  7682  findsg  7720  funcnvuni  7752  opabex3d  7781  opabex3rd  7782  opabex3  7783  1stconst  7911  2ndconst  7912  frxp  7938  soxp  7941  suppvalbr  7952  suppofssd  7990  suppcoss  7994  mpoxopovel  8007  brtpos  8022  tpostpos  8033  dfsmo2  8149  dfrecs3  8174  dfrecs3OLD  8175  rdglem1  8217  tz7.49  8246  brwitnlem  8299  oeeu  8396  erinxp  8538  mapsncnv  8639  cbvixp  8660  ixpin  8669  ixpiin  8670  mptelixpg  8681  elixpsn  8683  ixpsnf1o  8684  xpassen  8806  omxpenlem  8813  sbthcl  8835  sbthfilem  8941  wemapsolem  9239  dford2  9308  inf2  9311  zfinf  9327  trpredmintr  9409  trcl  9417  frind  9439  frr3g  9445  iscard2  9665  leweon  9698  aceq1  9804  dfac3  9808  dfac4  9809  dfac5lem2  9811  dfac5  9815  kmlem3  9839  kmlem4  9840  kmlem14  9850  kmlem15  9851  dfackm  9853  infmap2  9905  fin23lem25  10011  zorn2lem7  10189  brdom6disj  10219  zfcndrep  10301  zfcndinf  10305  fpwwe  10333  axgroth4  10519  grothprim  10521  grothtsk  10522  nqpr  10701  addsrmo  10760  mulsrmo  10761  opelreal  10817  elnnz  12259  elznn0nn  12263  peano2uz2  12338  nnwos  12584  dflt2  12811  xmullem  12927  4fvwrd4  13305  preduz  13307  elfznelfzo  13420  fzind2  13433  fsuppmapnn0fiubex  13640  hashinfxadd  14028  hashgt23el  14067  hashfun  14080  fi1uzind  14139  brfi1uzind  14140  opfi1uzind  14143  cotr2g  14615  shftdm  14710  rexfiuz  14987  cbvsum  15335  mertenslem2  15525  mertens  15526  cbvprod  15553  prodmo  15574  iprodmul  15641  divalglem10  16039  ndvdssub  16046  bitsmod  16071  algcvgblem  16210  isprm2  16315  isprm4  16317  hashdvds  16404  infpn2  16542  hashbc0  16634  xpscf  17193  funcpropd  17532  isffth2  17548  eldmcoa  17696  setcinv  17721  xpccatid  17821  yonedainv  17915  ispos  17947  ispos2  17948  joinfval2  18007  meetfval2  18021  istsr2  18217  isnsg2  18699  isnsg4  18710  isgim  18793  oppgid  18878  oppgcntz  18886  symgfix2  18939  efgval2  19245  iscyg2  19397  dmdprdd  19517  subgdmdprd  19552  issrg  19658  oppr1  19791  opprunit  19818  opprirred  19859  isrhm  19880  subsubrg2  19966  islmim  20239  lbsextg  20339  lidlnz  20412  isdomn2  20483  resubdrg  20725  unocv  20797  pjfval2  20826  islinds2  20930  opsrtoslem1  21172  mdetunilem8  21676  istop2g  21953  isbasis2g  22006  tgval2  22014  isclo2  22147  isnrm2  22417  is1stc2  22501  llyi  22533  isfbas2  22894  elfg  22930  ufinffr  22988  isfcls  23068  alexsubALTlem2  23107  alexsubALTlem3  23108  cnextcn  23126  ustfilxp  23272  iscusp2  23362  metustid  23616  isclmp  24166  iscvsp  24197  tcphcph  24306  iscau3  24347  caucfil  24352  mdegleb  25134  ellogdm  25699  dvdsflsumcom  26242  logfac2  26270  dchrelbas3  26291  dchrvmasumlema  26553  legtrid  26856  outpasch  27020  axcontlem5  27239  axcontlem6  27240  axcontlem7  27241  nb3grpr2  27653  iscplgr  27685  pthdlem1  28035  wwlksnextinj  28165  usgr2wspthon  28231  rusgrnumwwlkl1  28234  isclwwlk  28249  clwwlkccatlem  28254  clwwlknon2x  28368  iseupthf1o  28467  frcond3  28534  frgr3v  28540  4cycl2vnunb  28555  frgrncvvdeqlem2  28565  fusgr2wsp2nb  28599  numclwlk1lem1  28634  hhcms  29466  isch3  29504  ocsh  29546  pjhtheu  29657  pjpreeq  29661  h1deoi  29812  h1dei  29813  eleigvec  30220  cvbr2  30546  cvnbtwn2  30550  cvnbtwn4  30552  mdsl2i  30585  cvmdi  30587  mdsymlem6  30671  cdj3lem3b  30703  mo5f  30738  nmo  30739  rexunirn  30741  dmrab  30745  difrab2  30746  disjunsn  30834  unipreima  30882  dfcnv2  30915  1stpreima  30941  lsmsnorb2  31482  prmidl0  31528  ssmxidl  31544  zarcls  31726  rhmpreimacnlem  31736  isrnsiga  31981  rossros  32048  omsmeas  32190  eulerpartlemr  32241  eulerpartlemgvv  32243  ballotlemodife  32364  plymulx  32427  signstfvneq0  32451  bnj251  32581  bnj252  32582  bnj257  32586  bnj290  32589  bnj1304  32699  bnj153  32760  bnj543  32773  bnj571  32786  bnj580  32793  bnj607  32796  bnj882  32806  bnj964  32823  bnj996  32836  bnj1033  32849  bnj1176  32885  bnj1186  32887  bnj1189  32889  bnj1204  32892  bnj1253  32897  bnj1452  32932  bnj1463  32935  dff15  32956  fineqvrep  32964  fineqvac  32966  lfuhgr3  32981  cusgredgex2  32984  usgrgt2cycl  32992  2cycl2d  33001  dfacycgr1  33006  erdszelem9  33061  cvmlift2lem9  33173  cvmlift2lem13  33177  satfvsucsuc  33227  satfdm  33231  satf0  33234  fmlasucdisj  33261  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  elmthm  33438  axinfprim  33547  axacprim  33548  xpab  33579  dfso2  33628  dford5reg  33664  dfon2lem5  33669  dfon2  33674  ttrclselem2  33712  xpord3lem  33722  nosupno  33833  noinfno  33848  noinfbnd1lem1  33853  dmscut  33932  made0  33984  brtxp2  34110  brpprod3a  34115  dfom5b  34141  brcart  34161  brimg  34166  funpartlem  34171  dfrecs2  34179  cgrxfr  34284  segletr  34343  trer  34432  fneval  34468  neifg  34487  df3nandALT1  34515  andnand1  34517  nandsym1  34538  bj-eu3f  34952  bj-csbsnlem  35015  bj-snsetex  35080  bj-elsngl  35085  bj-snglc  35086  bj-restuni  35195  bj-dfmpoa  35216  bj-imdirco  35288  mptsnunlem  35436  icorempo  35449  isbasisrelowllem2  35454  relowlpssretop  35462  rdgeqoa  35468  difunieq  35472  dffinxpf  35483  nlpineqsn  35506  curf  35682  finixpnum  35689  ptrest  35703  poimirlem1  35705  poimirlem14  35718  poimirlem16  35720  poimirlem19  35723  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimir  35737  cnambfre  35752  itg2addnc  35758  ftc1anc  35785  opropabco  35809  isdrngo1  36041  keridl  36117  ispridlc  36155  selconj  36185  eldmqsres  36348  cnvepres  36360  ecinn0  36412  alrmomorn  36417  moantr  36421  dfxrn2  36433  inxpxrn  36448  rnxrnres  36452  refrelredund4  36675  dferALTV2  36707  dfeldisj3  36757  prtlem70  36798  prtlem100  36800  prtlem15  36816  islshpat  36958  lcvbr2  36963  lcvbr3  36964  lcvnbtwn2  36968  ellkr  37030  cvrval2  37215  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrnbtwn4  37220  ishlat2  37294  lplnexatN  37504  islvol5  37520  dath  37677  pclfinclN  37891  lhpexle3  37953  4atex2  38018  4atex2-0bOLDN  38020  isltrn2N  38061  cdleme0nex  38231  cdleme22b  38282  cdlemg17pq  38613  cdlemg19  38625  cdlemg21  38627  cdlemg33d  38650  dibopelvalN  39084  dibopelval2  39086  dib1dim  39106  dicelval2N  39123  diclspsn  39135  lcdlss  39560  mapd1o  39589  3factsumint2  39958  3factsumint3  39959  3factsumint  39961  sticksstones16  40046  sticksstones21  40051  metakunt1  40053  mhphf  40208  mzpcompact2lem  40489  fz1eqin  40507  rexrabdioph  40532  expdiophlem1  40759  dford4  40767  fnwe2lem2  40792  fgraphopab  40951  ifpidg  40996  rp-fakeinunass  41020  rp-isfinite6  41023  dfsucon  41028  elinintrab  41074  elnonrel  41082  elmapintab  41093  dfrtrcl5  41126  imaiun1  41148  coiun1  41149  rfovcnvf1od  41501  andi3or  41521  uneqsn  41522  ntrneicls00  41588  rr-groth  41806  ismnushort  41808  rr-grothshortbi  41810  2sbc5g  41923  pm14.12  41928  2sb5nd  42069  uun2221  42322  uun2221p1  42323  uun2221p2  42324  2sb5ndVD  42419  2sb5ndALT  42441  disjinfi  42620  climuz  43175  dfxlim2  43279  cncfshift  43305  dvnmul  43374  dvnprodlem2  43378  ismbl3  43417  ismbl4  43424  stoweidlem26  43457  stoweidlem35  43466  fourierdlem54  43591  fourierdlem83  43620  fourierdlem100  43637  fourierdlem104  43641  fourierdlem109  43646  fourierdlem112  43649  smfpimcc  44228  fcoresf1ob  44454  f1cof1b  44456  f1ocof1ob  44460  2reu8i  44492  dfdfat2  44507  ffnaov  44578  an4com24  44647  4an21  44649  iccpartiltu  44762  prproropf1olem0  44842  isrnghm  45338  2zrngmmgm  45392  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  opeliun2xp  45556  pgrpgt2nabl  45590  islindeps  45682  lindslinindsimp1  45686  lindslinindsimp2  45692  ldepslinc  45738  blen1b  45822  i0oii  46101  io1ii  46102  iscnrm3lem3  46117  isthinc2  46191  isthinc3  46192  isthincd2  46207  dffun3f  46274  setrec1lem3  46281  elpglem3  46304  elpg  46305