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  2264  19.41  2272  2sb5  2312  dfsb7  2313  dfeumo  2562  mo4f  2593  eu3v  2596  eu6  2600  dfeu  2621  eu2  2635  eu4  2641  2mos  2675  2eu4  2680  r3ex  3202  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  reu2  3683  reu6  3684  reu4  3689  reu7  3690  rmo3f  3692  rmo4f  3693  2reu5lem3  3715  2reu5  3716  sbcimdv  3807  sbcg  3811  rmo3  3836  reuan  3844  dfpss2  4036  difdif  4082  raldifb  4096  inass  4173  dfss4  4215  dfin2  4217  indi  4230  indifdi  4240  undif3  4246  difin0ss  4321  inssdif0OLD  4323  2nreu  4402  2reu4lem  4479  rexdifpr  4620  reuprg0  4663  ssdifsn  4751  ssunpr  4794  uniprg  4883  uniun  4890  uniinOLD  4892  csbuni  4898  dfiun2g  4988  iunin2  5029  iundif2  5032  iindif2  5037  iinin2  5038  elpwpw  5062  axrep1  5233  axrep4v  5237  axrep4  5238  reusv2lem4  5363  eqvinop  5456  eqvinot  5457  opcom  5473  fconstmpt  5713  opeliunxp  5718  opeliun2xp  5719  xpundi  5720  elvvv  5727  opelinxp  5731  xpiindi  5812  elcnv2  5855  cnvuni  5868  dmuni  5896  brres  5977  dmres  6003  elidinxp  6036  restidsing  6045  elima3  6063  asymref  6110  imainss  6144  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  mptpreima  6239  coundir  6249  resco  6251  coass  6267  relrelss  6275  opreu2reurex  6297  dfpo2  6299  frpoind  6345  ordtri3or  6395  dffun2  6548  dffun6  6549  dffun3  6550  dffun4  6551  dffun5  6552  dffun6f  6553  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  7120  fsn2  7137  tpres  7207  fconstfv  7218  dff13f  7259  dff14a  7274  dff14b  7275  dff15  7276  isocnv2  7339  f1opr  7476  eloprabga  7529  ffnov  7546  eqfnov  7549  foov  7595  uniuni  7776  tfindsg  7872  findsg  7909  funcnvuni  7944  opabex3d  7977  opabex3rd  7978  opabex3  7979  1stconst  8111  2ndconst  8112  frxp  8138  soxp  8141  fnwe2lem3  8147  xpord3lem  8166  suppvalbr  8181  suppofssd  8220  suppcoss  8224  mpoxopovel  8237  brtpos  8252  tpostpos  8263  dfsmo2  8355  dfrecs3  8380  rdglem1  8423  tz7.49  8455  brwitnlem  8515  oeeu  8612  naddasslem2  8705  brinxper  8747  erinxp  8812  curf  8890  mapsncnv  8921  cbvixp  8942  cbvixpv  8943  ixpin  8951  ixpiin  8952  mptelixpg  8963  elixpsn  8965  ixpsnf1o  8966  xpassen  9090  omxpenlem  9097  sbthcl  9118  sbthfilem  9213  wemapsolem  9544  dford2  9621  inf2  9624  zfinf  9640  ttrclselem2  9727  trcl  9729  frind  9754  frr3g  9760  elhf3  9913  setrec1lem3  9969  dffun3f  9975  iscard2  10057  leweon  10090  aceq1  10196  dfac3  10200  dfac4  10201  dfac5lem2  10203  dfac5  10207  kmlem3  10231  kmlem4  10232  kmlem14  10242  kmlem15  10243  dfackm  10245  infmap2  10295  fin23lem25  10402  zorn2lem7  10580  brdom6disj  10611  zfcndrep  10699  zfcndinf  10703  fpwwe  10731  axgroth4  10917  grothprim  10919  grothtsk  10920  nqpr  11099  addsrmo  11158  mulsrmo  11159  opelreal  11215  elnnz  12703  elznn0nn  12707  peano2uz2  12787  nnwos  13042  dflt2  13277  xmullem  13394  4fvwrd4  13782  preduz  13784  elfznelfzo  13908  fzind2  13923  fsuppmapnn0fiubex  14135  hashinfxadd  14529  hashgt23el  14569  hashfun  14582  fi1uzind  14652  brfi1uzind  14653  opfi1uzind  14656  cotr2g  15129  shftdm  15224  rexfiuz  15515  cbvsum  15862  cbvsumv  15863  mertenslem2  16054  mertens  16055  cbvprod  16082  cbvprodv  16083  prodeq1i  16085  prodmo  16103  iprodmul  16170  divalglem10  16572  ndvdssub  16579  bitsmod  16606  algcvgblem  16752  isprm2  16857  isprm4  16859  hashdvds  16952  infpn2  17091  hashbc0  17183  xpscf  17737  funcpropd  18077  isffth2  18093  eldmcoa  18240  setcinv  18265  xpccatid  18362  yonedainv  18455  ispos  18488  ispos2  18489  joinfval2  18546  meetfval2  18560  istsr2  18758  isnsg2  19366  isnsg4  19377  isgim  19476  oppgid  19570  oppgcntz  19578  symgfix2  19630  efgval2  19938  iscyg2  20096  dmdprdd  20215  subgdmdprd  20250  issrg  20414  dfring3  20518  oppr1  20580  opprunit  20607  opprirred  20652  isrnghm  20671  isrhm  20709  dfric2  20757  issubrng  20799  subsubrng2  20816  subsubrg2  20851  rngcinv  20889  ringcinv  20923  isdomn2  20963  islmim  21337  lbsextg  21440  lidlnz  21530  prmidl0  21634  resubdrg  21914  unocv  21986  pjfval2  22015  islinds2  22119  opsrtoslem1  22364  mdetunilem8  22934  istop2g  23214  isbasis2g  23266  tgval2  23274  isclo2  23406  isnrm2  23676  is1stc2  23760  llyi  23793  isfbas2  24154  elfg  24190  ufinffr  24248  isfcls  24328  alexsubALTlem2  24367  alexsubALTlem3  24368  cnextcn  24386  ustfilxp  24532  iscusp2  24620  metustid  24873  isclmp  25418  iscvsp  25449  tcphcph  25558  iscau3  25599  caucfil  25604  mdegleb  26382  plymulidp  26603  ellogdm  26967  dvdsflsumcom  27515  logfac2  27544  dchrelbas3  27565  dchrvmasumlema  27827  nosupno  28060  noinfno  28075  noinfbnd1lem1  28080  dmcuts  28177  made0  28249  mulsproplem5  28506  norecdiv  28576  elnnzs  28787  uzsind  28791  zsoring  28795  legtrid  29054  outpasch  29233  tgaaddcpbllem2  29350  tgaaddcpbllem3  29351  tgaltai  29445  axcontlem5  29546  axcontlem6  29547  axcontlem7  29548  lfuhgr3  29728  nb3grpr2  29964  iscplgr  29996  dfpth2  30314  pthdlem1  30352  wwlksnextinj  30488  usgr2wspthon  30557  rusgrnumwwlkl1  30560  isclwwlk  30575  clwwlkccatlem  30580  clwwlknon2x  30694  dfacycgr1  30750  iseupthf1o  30803  frcond3  30870  frgr3v  30876  4cycl2vnunb  30891  frgrncvvdeqlem2  30901  fusgr2wsp2nb  30935  numclwlk1lem1  30970  hhcms  31805  isch3  31843  ocsh  31885  pjhtheu  31996  pjpreeq  32000  h1deoi  32151  h1dei  32152  eleigvec  32559  cvbr2  32885  cvnbtwn2  32889  cvnbtwn4  32891  mdsl2i  32924  cvmdi  32926  mdsymlem6  33010  cdj3lem3b  33042  mo5f  33085  nmo  33086  rexunirn  33088  dmrab  33093  difrab2  33094  disjunsn  33188  unipreima  33237  dfcnv2  33269  1stpreima  33300  isunit2  33800  lsmsnorb2  33947  ssmxidl  33999  1arithufdlem4  34079  ressply1mon1p  34100  extdgfialglem1  34324  zarcls  34506  rhmpreimacnlem  34516  isrnsiga  34745  rossros  34813  omsmeas  34955  eulerpartlemr  35006  eulerpartlemgvv  35008  ballotlemodife  35130  signstfvneq0  35201  bnj251  35333  bnj252  35334  bnj257  35338  bnj290  35341  bnj1304  35449  bnj153  35510  bnj543  35523  bnj571  35536  bnj580  35543  bnj607  35546  bnj882  35556  bnj964  35573  bnj996  35586  bnj1033  35599  bnj1176  35635  bnj1186  35637  bnj1189  35639  bnj1204  35642  bnj1253  35647  bnj1452  35682  bnj1463  35685  r1omhf  35731  axprALT2  35734  fineqvrep  35782  fineqvac  35784  kardexen  35831  onprcf1acwevdlem1  35895  cusgredgex2  35907  usgrgt2cycl  35909  2cycl2d  35912  erdszelem9  35964  cvmlift2lem9  36076  cvmlift2lem13  36080  satfvsucsuc  36130  satfdm  36134  satf0  36137  fmlasucdisj  36164  satffunlem  36166  satffunlem1lem1  36167  satffunlem2lem1  36169  elmthm  36341  axinfprim  36471  axacprim  36472  xpab  36491  dfso2  36520  dford5reg  36544  dfon2lem5  36549  dfon2  36554  brtxp2  36643  brpprod3a  36648  dfom5b  36674  brcart  36694  brimg  36699  funpartlem  36706  dfrecs2  36714  cgrxfr  36820  segletr  36879  sumeq2si  36991  prodeq2si  36993  cbvprodvw2  37036  trer  37104  fneval  37140  neifg  37159  df3nandALT1  37187  andnand1  37189  nandsym1  37210  weiunlem  37251  regsfromregtco  37326  mh-infprim2bi  37335  mh-infprim3bi  37336  bj-df-sb  37549  bj-dfsbc  37551  bj-eu3f  37753  bj-csbsnlem  37815  bj-snsetex  37876  bj-elsngl  37881  bj-snglc  37882  coi1in  37961  bj-restuni  38018  bj-dfmpoa  38039  bj-imdirco  38111  mptsnunlem  38261  icorempo  38274  isbasisrelowllem2  38279  relowlpssretop  38287  rdgeqoa  38293  difunieq  38297  dffinxpf  38308  nlpineqsn  38331  finixpnum  38528  ptrest  38537  poimirlem1  38539  poimirlem14  38552  poimirlem16  38554  poimirlem19  38557  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  poimir  38571  cnambfre  38586  itg2addnc  38592  ftc1anc  38619  dfprop1  38645  opropabco  38658  isdrngo1  38890  keridl  38966  ispridlc  39004  selconj  39032  eldmres3  39215  eldmqsres  39225  cnvepres  39236  ecinn0  39285  alrmomorn  39290  moantr  39304  dfxrn2  39317  disjressuc2  39343  inxpxrn  39350  rnxrnres  39354  coss2cnvepres  39440  refrelredund4  39651  dferALTV2  39685  dfeldisj3  39743  dfpart2  39804  dfpeters2  39906  petseq  39908  prtlem70  39914  prtlem100  39916  prtlem15  39932  islshpat  40074  lcvbr2  40079  lcvbr3  40080  lcvnbtwn2  40084  ellkr  40146  cvrval2  40331  cvrnbtwn2  40332  cvrnbtwn3  40333  cvrnbtwn4  40336  ishlat2  40410  lplnexatN  40620  islvol5  40636  dath  40793  pclfinclN  41007  lhpexle3  41069  4atex2  41134  4atex2-0bOLDN  41136  isltrn2N  41177  cdleme0nex  41347  cdleme22b  41398  cdlemg17pq  41729  cdlemg19  41741  cdlemg21  41743  cdlemg33d  41766  dibopelvalN  42200  dibopelval2  42202  dib1dim  42222  dicelval2N  42239  diclspsn  42251  lcdlss  42676  mapd1o  42705  3factsumint2  43072  3factsumint3  43073  3factsumint  43075  hashnexinj  43178  sticksstones16  43212  sticksstones21  43217  unitscyglem3  43247  supinf  43293  fimgmcyclem  43597  eu6w  43687  mzpcompact2lem  43761  fz1eqin  43779  rexrabdioph  43800  expdiophlem1  44027  dford4  44035  fgraphopab  44204  dflim6  44265  onsucf1olem  44271  onsucrn  44272  nnoeomeqom  44313  faosnf0.11b  44427  ifpidg  44491  rp-fakeinunass  44515  rp-isfinite6  44518  dfsucon  44523  elinintrab  44577  elnonrel  44585  elmapintab  44595  dfrtrcl5  44628  imaiun1  44650  coiun1  44651  rfovcnvf1od  45003  andi3or  45023  uneqsn  45024  ntrneicls00  45088  rr-groth  45282  ismnushort  45284  rr-grothshortbi  45286  2sbc5g  45399  pm14.12  45404  2sb5nd  45542  uun2221  45794  uun2221p1  45795  uun2221p2  45796  2sb5ndVD  45891  2sb5ndALT  45913  modelaxreplem3  45969  iindif2f  46174  disjinfi  46206  climuz  46753  dfxlim2  46857  cncfshift  46883  dvnmul  46952  dvnprodlem2  46956  ismbl3  46995  ismbl4  47002  stoweidlem26  47035  stoweidlem35  47044  fourierdlem54  47169  fourierdlem83  47198  fourierdlem100  47215  fourierdlem104  47219  fourierdlem109  47224  fourierdlem112  47227  smfpimcc  47817  fcoresf1ob  48142  f1cof1b  48146  f1ocof1ob  48150  2reu8i  48182  dfdfat2  48197  ffnaov  48268  an4com24  48337  4an21  48339  iccpartiltu  48503  prproropf1olem0  48583  dfgric2  49012  gpgvtxedg0  49160  gpgvtxedg1  49161  gpgprismgr4cycllem10  49201  grlimedgnedg  49228  2zrngmmgm  49348  rngcinvALTV  49372  ringcinvALTV  49406  isprmrng  49432  pgrpgt2nabl  49477  islindeps  49564  lindslinindsimp1  49568  lindslinindsimp2  49574  ldepslinc  49620  blen1b  49699  coxp  49942  i0oii  50027  io1ii  50028  isthinc2  50527  isthinc3  50528  isthincd2  50544  istermc2  50582  istermc3  50583  elpglem3  50805  elpg  50806  alsanmo  50905  ralsanmo  50906  2alsraln0  50912  2alsraln0id  50913