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

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  anbi1ci  626  anbi12i  628  bianass  642  an42  657  anandir  677  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  4anpull2  1362  an3andi  1484  an33rean  1485  anxordi  1526  cadcoma  1612  nic-mpALT  1672  nic-axALT  1674  3exdistr  1960  4exdistr  1961  19.27v  1995  19.27  2228  19.41  2236  2sb5  2278  dfsb7  2279  dfeumo  2530  mo4f  2560  eu3v  2563  eu6  2567  dfeu  2588  eu2  2602  eu4  2608  2mos  2642  2mosOLD  2643  2eu4  2648  r3ex  3168  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  reu2  3685  reu6  3686  reu4  3691  reu7  3692  rmo3f  3694  rmo4f  3695  2reu5lem3  3717  2reu5  3718  sbcimdv  3811  sbcg  3815  rmo3  3841  reuan  3848  dfpss2  4039  difdif  4086  raldifb  4100  inass  4179  dfss4  4220  dfin2  4222  indi  4235  indifdi  4245  undif3  4251  difin0ss  4324  inssdif0  4325  2nreu  4395  2reu4lem  4473  rexdifpr  4611  reuprg0  4654  ssdifsn  4739  ssunpr  4785  uniprg  4874  uniun  4881  uniin  4882  csbuni  4887  dfiun2g  4980  iunin2  5020  iundif2  5023  iindif2  5026  iinin2  5027  elpwpw  5051  axrep1  5219  axrep4v  5223  axrep4  5224  axrep4OLD  5225  reusv2lem4  5340  eqvinop  5430  opcom  5444  fconstmpt  5681  opeliunxp  5686  opeliun2xp  5687  xpundi  5688  elvvv  5695  opelinxp  5699  xpiindi  5778  elcnv2  5820  cnvuni  5829  dmuni  5857  brres  5937  dmres  5963  elidinxp  5995  restidsing  6004  elima3  6018  asymref  6065  imainss  6103  difxp  6113  xpdifid  6117  mptpreima  6187  coundir  6197  resco  6199  coass  6214  relrelss  6221  opreu2reurex  6242  dfpo2  6244  frpoind  6290  ordtri3or  6339  dffun2  6492  dffun6  6493  dffun3  6494  dffun4  6495  dffun5  6496  dffun6f  6497  dffun7  6509  dffun8  6510  dffun9  6511  svrelfun  6554  fncnv  6555  imadif  6566  dfmpt3  6616  fcnvres  6701  fint  6703  fin  6704  dff12  6719  fores  6746  dff1o4  6772  eqfnfv3  6967  fndmin  6979  fniniseg  6994  unpreima  6997  ffnfvf  7054  fsn2  7070  tpres  7137  fconstfv  7148  dff13f  7192  dff14a  7207  dff14b  7208  isocnv2  7268  f1opr  7405  eloprabga  7458  ffnov  7475  eqfnov  7478  foov  7523  uniuni  7698  tfindsg  7794  findsg  7830  funcnvuni  7865  opabex3d  7900  opabex3rd  7901  opabex3  7902  1stconst  8033  2ndconst  8034  frxp  8059  soxp  8062  xpord3lem  8082  suppvalbr  8097  suppofssd  8136  suppcoss  8140  mpoxopovel  8153  brtpos  8168  tpostpos  8179  dfsmo2  8270  dfrecs3  8295  rdglem1  8337  tz7.49  8367  brwitnlem  8425  oeeu  8521  naddasslem2  8613  brinxper  8654  erinxp  8718  mapsncnv  8820  cbvixp  8841  cbvixpv  8842  ixpin  8850  ixpiin  8851  mptelixpg  8862  elixpsn  8864  ixpsnf1o  8865  xpassen  8988  omxpenlem  8995  sbthcl  9016  sbthfilem  9112  wemapsolem  9442  dford2  9516  inf2  9519  zfinf  9535  ttrclselem2  9622  trcl  9624  frind  9646  frr3g  9652  iscard2  9872  leweon  9905  aceq1  10011  dfac3  10015  dfac4  10016  dfac5lem2  10018  dfac5  10023  kmlem3  10047  kmlem4  10048  kmlem14  10058  kmlem15  10059  dfackm  10061  infmap2  10111  fin23lem25  10218  zorn2lem7  10396  brdom6disj  10426  zfcndrep  10508  zfcndinf  10512  fpwwe  10540  axgroth4  10726  grothprim  10728  grothtsk  10729  nqpr  10908  addsrmo  10967  mulsrmo  10968  opelreal  11024  elnnz  12481  elznn0nn  12485  peano2uz2  12564  nnwos  12816  dflt2  13050  xmullem  13166  4fvwrd4  13551  preduz  13553  elfznelfzo  13675  fzind2  13688  fsuppmapnn0fiubex  13899  hashinfxadd  14292  hashgt23el  14331  hashfun  14344  fi1uzind  14414  brfi1uzind  14415  opfi1uzind  14418  cotr2g  14883  shftdm  14978  rexfiuz  15255  cbvsum  15602  cbvsumv  15603  mertenslem2  15792  mertens  15793  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  prodmo  15843  iprodmul  15910  divalglem10  16313  ndvdssub  16320  bitsmod  16347  algcvgblem  16488  isprm2  16593  isprm4  16595  hashdvds  16686  infpn2  16825  hashbc0  16917  xpscf  17469  funcpropd  17809  isffth2  17825  eldmcoa  17972  setcinv  17997  xpccatid  18094  yonedainv  18187  ispos  18220  ispos2  18221  joinfval2  18278  meetfval2  18292  istsr2  18490  isnsg2  19035  isnsg4  19046  isgim  19141  oppgid  19235  oppgcntz  19243  symgfix2  19295  efgval2  19603  iscyg2  19761  dmdprdd  19880  subgdmdprd  19915  issrg  20073  oppr1  20235  opprunit  20262  opprirred  20307  isrnghm  20326  isrhm  20363  issubrng  20432  subsubrng2  20449  subsubrg2  20484  rngcinv  20522  ringcinv  20556  isdomn2  20596  isdomn2OLD  20597  islmim  20966  lbsextg  21069  lidlnz  21149  resubdrg  21515  unocv  21587  pjfval2  21616  islinds2  21720  opsrtoslem1  21960  mdetunilem8  22504  istop2g  22781  isbasis2g  22833  tgval2  22841  isclo2  22973  isnrm2  23243  is1stc2  23327  llyi  23359  isfbas2  23720  elfg  23756  ufinffr  23814  isfcls  23894  alexsubALTlem2  23933  alexsubALTlem3  23934  cnextcn  23952  ustfilxp  24098  iscusp2  24187  metustid  24440  isclmp  24995  iscvsp  25026  tcphcph  25135  iscau3  25176  caucfil  25181  mdegleb  25967  ellogdm  26546  dvdsflsumcom  27096  logfac2  27126  dchrelbas3  27147  dchrvmasumlema  27409  nosupno  27613  noinfno  27628  noinfbnd1lem1  27633  dmscut  27722  made0  27787  mulsproplem5  28028  norecdiv  28098  elnnzs  28294  uzsind  28298  zsoring  28301  legtrid  28536  outpasch  28700  axcontlem5  28913  axcontlem6  28914  axcontlem7  28915  nb3grpr2  29328  iscplgr  29360  dfpth2  29674  pthdlem1  29711  wwlksnextinj  29844  usgr2wspthon  29910  rusgrnumwwlkl1  29913  isclwwlk  29928  clwwlkccatlem  29933  clwwlknon2x  30047  iseupthf1o  30146  frcond3  30213  frgr3v  30219  4cycl2vnunb  30234  frgrncvvdeqlem2  30244  fusgr2wsp2nb  30278  numclwlk1lem1  30313  hhcms  31147  isch3  31185  ocsh  31227  pjhtheu  31338  pjpreeq  31342  h1deoi  31493  h1dei  31494  eleigvec  31901  cvbr2  32227  cvnbtwn2  32231  cvnbtwn4  32233  mdsl2i  32266  cvmdi  32268  mdsymlem6  32352  cdj3lem3b  32384  mo5f  32433  nmo  32434  rexunirn  32436  dmrab  32441  difrab2  32442  disjunsn  32538  unipreima  32586  dfcnv2  32619  1stpreima  32649  isunit2  33180  lsmsnorb2  33329  prmidl0  33387  ssmxidl  33411  1arithufdlem4  33484  ressply1mon1p  33503  extdgfialglem1  33659  zarcls  33841  rhmpreimacnlem  33851  isrnsiga  34080  rossros  34147  omsmeas  34291  eulerpartlemr  34342  eulerpartlemgvv  34344  ballotlemodife  34466  plymulx  34516  signstfvneq0  34540  bnj251  34669  bnj252  34670  bnj257  34674  bnj290  34677  bnj1304  34786  bnj153  34847  bnj543  34860  bnj571  34873  bnj580  34880  bnj607  34883  bnj882  34893  bnj964  34910  bnj996  34923  bnj1033  34936  bnj1176  34972  bnj1186  34974  bnj1189  34976  bnj1204  34979  bnj1253  34984  bnj1452  35019  bnj1463  35022  dff15  35051  fineqvrep  35070  fineqvac  35072  lfuhgr3  35093  cusgredgex2  35096  usgrgt2cycl  35103  2cycl2d  35112  dfacycgr1  35117  erdszelem9  35172  cvmlift2lem9  35284  cvmlift2lem13  35288  satfvsucsuc  35338  satfdm  35342  satf0  35345  fmlasucdisj  35372  satffunlem  35374  satffunlem1lem1  35375  satffunlem2lem1  35377  elmthm  35549  axinfprim  35679  axacprim  35680  xpab  35699  dfso2  35728  dford5reg  35756  dfon2lem5  35761  dfon2  35766  brtxp2  35855  brpprod3a  35860  dfom5b  35886  brcart  35906  brimg  35911  funpartlem  35916  dfrecs2  35924  cgrxfr  36029  segletr  36088  sumeq2si  36176  prodeq2si  36178  cbvprodvw2  36221  trer  36290  fneval  36326  neifg  36345  df3nandALT1  36373  andnand1  36375  nandsym1  36396  weiunlem2  36437  bj-eu3f  36815  bj-csbsnlem  36877  bj-snsetex  36937  bj-elsngl  36942  bj-snglc  36943  bj-restuni  37071  bj-dfmpoa  37092  bj-imdirco  37164  mptsnunlem  37312  icorempo  37325  isbasisrelowllem2  37330  relowlpssretop  37338  rdgeqoa  37344  difunieq  37348  dffinxpf  37359  nlpineqsn  37382  curf  37578  finixpnum  37585  ptrest  37599  poimirlem1  37601  poimirlem14  37614  poimirlem16  37616  poimirlem19  37619  poimirlem25  37625  poimirlem26  37626  poimirlem27  37627  poimir  37633  cnambfre  37648  itg2addnc  37654  ftc1anc  37681  opropabco  37704  isdrngo1  37936  keridl  38012  ispridlc  38050  selconj  38080  eldmres3  38251  eldmqsres  38261  cnvepres  38272  ecinn0  38321  alrmomorn  38326  moantr  38332  dfxrn2  38344  disjressuc2  38360  inxpxrn  38367  rnxrnres  38371  coss2cnvepres  38395  refrelredund4  38612  dferALTV2  38646  dfeldisj3  38697  dfpart2  38747  prtlem70  38836  prtlem100  38838  prtlem15  38854  islshpat  38996  lcvbr2  39001  lcvbr3  39002  lcvnbtwn2  39006  ellkr  39068  cvrval2  39253  cvrnbtwn2  39254  cvrnbtwn3  39255  cvrnbtwn4  39258  ishlat2  39332  lplnexatN  39542  islvol5  39558  dath  39715  pclfinclN  39929  lhpexle3  39991  4atex2  40056  4atex2-0bOLDN  40058  isltrn2N  40099  cdleme0nex  40269  cdleme22b  40320  cdlemg17pq  40651  cdlemg19  40663  cdlemg21  40665  cdlemg33d  40688  dibopelvalN  41122  dibopelval2  41124  dib1dim  41144  dicelval2N  41161  diclspsn  41173  lcdlss  41598  mapd1o  41627  3factsumint2  41995  3factsumint3  41996  3factsumint  41998  hashnexinj  42101  sticksstones16  42135  sticksstones21  42140  unitscyglem3  42170  supinf  42215  fimgmcyclem  42506  eu6w  42649  mzpcompact2lem  42724  fz1eqin  42742  rexrabdioph  42767  expdiophlem1  42994  dford4  43002  fnwe2lem2  43024  fgraphopab  43176  dflim6  43237  onsucf1olem  43243  onsucrn  43244  nnoeomeqom  43285  faosnf0.11b  43400  ifpidg  43464  rp-fakeinunass  43488  rp-isfinite6  43491  dfsucon  43496  elinintrab  43550  elnonrel  43558  elmapintab  43569  dfrtrcl5  43602  imaiun1  43624  coiun1  43625  rfovcnvf1od  43977  andi3or  43997  uneqsn  43998  ntrneicls00  44062  rr-groth  44272  ismnushort  44274  rr-grothshortbi  44276  2sbc5g  44389  pm14.12  44394  2sb5nd  44534  uun2221  44786  uun2221p1  44787  uun2221p2  44788  2sb5ndVD  44883  2sb5ndALT  44905  modelaxreplem3  44954  iindif2f  45138  disjinfi  45170  climuz  45725  dfxlim2  45829  cncfshift  45855  dvnmul  45924  dvnprodlem2  45928  ismbl3  45967  ismbl4  45974  stoweidlem26  46007  stoweidlem35  46016  fourierdlem54  46141  fourierdlem83  46170  fourierdlem100  46187  fourierdlem104  46191  fourierdlem109  46196  fourierdlem112  46199  smfpimcc  46789  fcoresf1ob  47057  f1cof1b  47061  f1ocof1ob  47065  2reu8i  47097  dfdfat2  47112  ffnaov  47183  an4com24  47252  4an21  47254  iccpartiltu  47406  prproropf1olem0  47486  dfgric2  47899  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem10  48088  grlimedgnedg  48115  2zrngmmgm  48236  rngcinvALTV  48260  ringcinvALTV  48294  pgrpgt2nabl  48350  islindeps  48438  lindslinindsimp1  48442  lindslinindsimp2  48448  ldepslinc  48494  blen1b  48573  coxp  48817  i0oii  48904  io1ii  48905  isthinc2  49405  isthinc3  49406  isthincd2  49422  istermc2  49460  istermc3  49461  dffun3f  49667  setrec1lem3  49674  elpglem3  49698  elpg  49699