Theorem anbi2i 626

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi1ci  629  anbi12i  630  bianass  642  an42  657  anandir  677  dfbi3  1050  dn1  1058  dfifp3  1066  ifpdfbi  1071  an3andi  1484  an33rean  1485  an33reanOLD  1486  anxordi  1524  norassOLD  1540  cadcoma  1619  nic-mpALT  1680  nic-axALT  1682  3exdistr  1969  4exdistr  1970  19.27v  1998  19.27  2225  19.41  2233  2sb5  2276  dfsb7  2280  dfeumo  2536  mo4f  2566  eu3v  2569  eu6  2573  dfeu  2594  eu2  2610  eu4  2616  2mos  2650  2eu4  2655  ceqsex3v  3460  ceqsex4v  3461  ceqsex8v  3463  reu2  3638  reu6  3639  reu4  3644  reu7  3645  rmo3f  3647  rmo4f  3648  2reu5lem3  3670  2reu5  3671  sbcimdv  3769  sbcg  3774  rmo3  3801  reuan  3808  dfpss2  4000  difdif  4045  raldifb  4059  inass  4134  dfss4  4173  dfin2  4175  indi  4188  indifdi  4198  indifdirOLD  4200  undif3  4205  difin0ss  4283  inssdif0  4284  2nreu  4356  2reu4lem  4437  rexdifpr  4574  reuprg0  4618  ssdifsn  4701  ssunpr  4745  uniprg  4836  uniprOLD  4838  uniun  4844  uniin  4845  csbuni  4850  iunin2  4979  iundif2  4982  iindif2  4985  iinin2  4986  elpwpw  5010  axrep1  5180  axrep4  5184  notzfausOLD  5255  reusv2lem4  5294  eqvinop  5370  opcom  5384  fconstmpt  5611  opeliunxp  5616  xpundi  5617  elvvv  5624  opelinxp  5628  xpiindi  5704  elcnv2  5746  cnvuni  5755  dmuni  5783  brres  5858  dmres  5873  elidinxp  5911  restidsing  5922  elima3  5936  asymref  5981  imainss  6017  difxp  6027  xpdifid  6031  mptpreima  6101  coundir  6112  resco  6114  coass  6129  relrelss  6136  opreu2reurex  6157  frpoind  6196  wfi  6203  ordtri3or  6245  dffun2  6390  dffun3  6391  dffun4  6392  dffun5  6393  dffun6f  6394  dffun7  6407  dffun8  6408  dffun9  6409  svrelfun  6452  fncnv  6453  imadif  6464  dfmpt3  6512  fcnvres  6596  fint  6598  fin  6599  dff12  6614  fores  6643  dff1o4  6669  eqfnfv3  6854  fndmin  6865  fniniseg  6880  unpreima  6883  ffnfvf  6936  fsn2  6951  tpres  7016  fconstfv  7028  dff13f  7068  dff14a  7082  dff14b  7083  isocnv2  7140  f1opr  7267  eloprabga  7318  ffnov  7337  eqfnov  7339  foov  7382  uniuni  7547  tfindsg  7639  findsg  7677  funcnvuni  7709  opabex3d  7738  opabex3rd  7739  opabex3  7740  1stconst  7868  2ndconst  7869  frxp  7893  soxp  7896  suppvalbr  7907  suppofssd  7945  suppcoss  7949  mpoxopovel  7962  brtpos  7977  tpostpos  7988  dfsmo2  8084  dfrecs3  8109  rdglem1  8151  tz7.49  8181  brwitnlem  8234  oeeu  8331  erinxp  8473  mapsncnv  8574  cbvixp  8595  ixpin  8604  ixpiin  8605  mptelixpg  8616  elixpsn  8618  ixpsnf1o  8619  xpassen  8739  omxpenlem  8746  sbthcl  8768  wemapsolem  9166  dford2  9235  inf2  9238  zfinf  9254  trpredmintr  9336  trcl  9344  frind  9366  frr3g  9372  iscard2  9592  leweon  9625  aceq1  9731  dfac3  9735  dfac4  9736  dfac5lem2  9738  dfac5  9742  kmlem3  9766  kmlem4  9767  kmlem14  9777  kmlem15  9778  dfackm  9780  infmap2  9832  fin23lem25  9938  zorn2lem7  10116  brdom6disj  10146  zfcndrep  10228  zfcndinf  10232  fpwwe  10260  axgroth4  10446  grothprim  10448  grothtsk  10449  nqpr  10628  addsrmo  10687  mulsrmo  10688  opelreal  10744  elnnz  12186  elznn0nn  12190  peano2uz2  12265  nnwos  12511  dflt2  12738  xmullem  12854  4fvwrd4  13232  preduz  13234  elfznelfzo  13347  fzind2  13360  fsuppmapnn0fiubex  13565  hashinfxadd  13952  hashgt23el  13991  hashfun  14004  fi1uzind  14063  brfi1uzind  14064  opfi1uzind  14067  cotr2g  14539  shftdm  14634  rexfiuz  14911  cbvsum  15259  mertenslem2  15449  mertens  15450  cbvprod  15477  prodmo  15498  iprodmul  15565  divalglem10  15963  ndvdssub  15970  bitsmod  15995  algcvgblem  16134  isprm2  16239  isprm4  16241  hashdvds  16328  infpn2  16466  hashbc0  16558  xpscf  17070  funcpropd  17407  isffth2  17423  eldmcoa  17571  setcinv  17596  xpccatid  17695  yonedainv  17789  ispos  17821  ispos2  17822  joinfval2  17880  meetfval2  17894  istsr2  18090  isnsg2  18572  isnsg4  18583  isgim  18666  oppgid  18748  oppgcntz  18756  symgfix2  18808  efgval2  19114  iscyg2  19266  dmdprdd  19386  subgdmdprd  19421  issrg  19522  oppr1  19652  opprunit  19679  opprirred  19720  isrhm  19741  subsubrg2  19827  islmim  20099  lbsextg  20199  lidlnz  20266  isdomn2  20337  resubdrg  20570  unocv  20642  pjfval2  20671  islinds2  20775  opsrtoslem1  21012  mdetunilem8  21516  istop2g  21793  isbasis2g  21845  tgval2  21853  isclo2  21985  isnrm2  22255  is1stc2  22339  llyi  22371  isfbas2  22732  elfg  22768  ufinffr  22826  isfcls  22906  alexsubALTlem2  22945  alexsubALTlem3  22946  cnextcn  22964  ustfilxp  23110  iscusp2  23199  metustid  23452  isclmp  23994  iscvsp  24025  tcphcph  24134  iscau3  24175  caucfil  24180  mdegleb  24962  ellogdm  25527  dvdsflsumcom  26070  logfac2  26098  dchrelbas3  26119  dchrvmasumlema  26381  legtrid  26682  outpasch  26846  axcontlem5  27059  axcontlem6  27060  axcontlem7  27061  nb3grpr2  27471  iscplgr  27503  pthdlem1  27853  wwlksnextinj  27983  usgr2wspthon  28049  rusgrnumwwlkl1  28052  isclwwlk  28067  clwwlkccatlem  28072  clwwlknon2x  28186  iseupthf1o  28285  frcond3  28352  frgr3v  28358  4cycl2vnunb  28373  frgrncvvdeqlem2  28383  fusgr2wsp2nb  28417  numclwlk1lem1  28452  hhcms  29284  isch3  29322  ocsh  29364  pjhtheu  29475  pjpreeq  29479  h1deoi  29630  h1dei  29631  eleigvec  30038  cvbr2  30364  cvnbtwn2  30368  cvnbtwn4  30370  mdsl2i  30403  cvmdi  30405  mdsymlem6  30489  cdj3lem3b  30521  mo5f  30556  nmo  30557  rexunirn  30559  dmrab  30563  difrab2  30564  disjunsn  30652  unipreima  30700  dfcnv2  30733  1stpreima  30759  lsmsnorb2  31294  prmidl0  31340  ssmxidl  31356  zarcls  31538  rhmpreimacnlem  31548  isrnsiga  31793  rossros  31860  omsmeas  32002  eulerpartlemr  32053  eulerpartlemgvv  32055  ballotlemodife  32176  plymulx  32239  signstfvneq0  32263  bnj251  32393  bnj252  32394  bnj257  32398  bnj290  32401  bnj1304  32512  bnj153  32573  bnj543  32586  bnj571  32599  bnj580  32606  bnj607  32609  bnj882  32619  bnj964  32636  bnj996  32649  bnj1033  32662  bnj1176  32698  bnj1186  32700  bnj1189  32702  bnj1204  32705  bnj1253  32710  bnj1452  32745  bnj1463  32748  dff15  32769  fineqvrep  32777  fineqvac  32779  lfuhgr3  32794  cusgredgex2  32797  usgrgt2cycl  32805  2cycl2d  32814  dfacycgr1  32819  erdszelem9  32874  cvmlift2lem9  32986  cvmlift2lem13  32990  satfvsucsuc  33040  satfdm  33044  satf0  33047  fmlasucdisj  33074  satffunlem  33076  satffunlem1lem1  33077  satffunlem2lem1  33079  elmthm  33251  axinfprim  33360  axacprim  33361  xpab  33392  dfso2  33440  dfpo2  33441  dford5reg  33477  dfon2lem5  33482  dfon2  33487  xpord3lem  33532  nosupno  33643  noinfno  33658  noinfbnd1lem1  33663  dmscut  33742  made0  33794  brtxp2  33920  brpprod3a  33925  dfom5b  33951  brcart  33971  brimg  33976  funpartlem  33981  dfrecs2  33989  cgrxfr  34094  segletr  34153  trer  34242  fneval  34278  neifg  34297  df3nandALT1  34325  andnand1  34327  nandsym1  34348  bj-eu3f  34762  bj-csbsnlem  34825  bj-snsetex  34890  bj-elsngl  34895  bj-snglc  34896  bj-restuni  35003  bj-dfmpoa  35024  bj-imdirco  35096  bj-isrvec  35199  mptsnunlem  35246  icorempo  35259  isbasisrelowllem2  35264  relowlpssretop  35272  rdgeqoa  35278  difunieq  35282  dffinxpf  35293  nlpineqsn  35316  curf  35492  finixpnum  35499  ptrest  35513  poimirlem1  35515  poimirlem14  35528  poimirlem16  35530  poimirlem19  35533  poimirlem25  35539  poimirlem26  35540  poimirlem27  35541  poimir  35547  cnambfre  35562  itg2addnc  35568  ftc1anc  35595  opropabco  35619  isdrngo1  35851  keridl  35927  ispridlc  35965  selconj  35995  eldmqsres  36158  cnvepres  36170  ecinn0  36222  alrmomorn  36227  moantr  36231  dfxrn2  36243  inxpxrn  36258  rnxrnres  36262  refrelredund4  36485  dferALTV2  36517  dfeldisj3  36567  prtlem70  36608  prtlem100  36610  prtlem15  36626  islshpat  36768  lcvbr2  36773  lcvbr3  36774  lcvnbtwn2  36778  ellkr  36840  cvrval2  37025  cvrnbtwn2  37026  cvrnbtwn3  37027  cvrnbtwn4  37030  ishlat2  37104  lplnexatN  37314  islvol5  37330  dath  37487  pclfinclN  37701  lhpexle3  37763  4atex2  37828  4atex2-0bOLDN  37830  isltrn2N  37871  cdleme0nex  38041  cdleme22b  38092  cdlemg17pq  38423  cdlemg19  38435  cdlemg21  38437  cdlemg33d  38460  dibopelvalN  38894  dibopelval2  38896  dib1dim  38916  dicelval2N  38933  diclspsn  38945  lcdlss  39370  mapd1o  39399  3factsumint2  39764  3factsumint3  39765  3factsumint  39767  sticksstones16  39840  sticksstones21  39845  metakunt1  39847  mhphf  39995  mzpcompact2lem  40276  fz1eqin  40294  rexrabdioph  40319  expdiophlem1  40546  dford4  40554  fnwe2lem2  40579  fgraphopab  40738  ifpidg  40783  rp-fakeinunass  40807  rp-isfinite6  40810  dfsucon  40815  elinintrab  40861  elnonrel  40869  elmapintab  40880  dfrtrcl5  40913  imaiun1  40936  coiun1  40937  rfovcnvf1od  41289  andi3or  41309  uneqsn  41310  ntrneicls00  41376  rr-groth  41590  ismnushort  41592  rr-grothshortbi  41594  2sbc5g  41707  pm14.12  41712  2sb5nd  41853  uun2221  42106  uun2221p1  42107  uun2221p2  42108  2sb5ndVD  42203  2sb5ndALT  42225  disjinfi  42404  climuz  42960  dfxlim2  43064  cncfshift  43090  dvnmul  43159  dvnprodlem2  43163  ismbl3  43202  ismbl4  43209  stoweidlem26  43242  stoweidlem35  43251  fourierdlem54  43376  fourierdlem83  43405  fourierdlem100  43422  fourierdlem104  43426  fourierdlem109  43431  fourierdlem112  43434  smfpimcc  44013  fcoresf1ob  44239  f1cof1b  44241  f1ocof1ob  44245  2reu8i  44277  dfdfat2  44292  ffnaov  44363  an4com24  44432  4an21  44434  iccpartiltu  44547  prproropf1olem0  44627  isrnghm  45123  2zrngmmgm  45177  rngcinv  45212  rngcinvALTV  45224  ringcinv  45263  ringcinvALTV  45287  opeliun2xp  45341  pgrpgt2nabl  45375  islindeps  45467  lindslinindsimp1  45471  lindslinindsimp2  45477  ldepslinc  45523  blen1b  45607  i0oii  45886  io1ii  45887  iscnrm3lem3  45902  isthinc2  45976  isthinc3  45977  isthincd2  45992  dffun3f  46059  setrec1lem3  46066  elpglem3  46089  elpg  46090