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  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  2270  dfsb7  2274  dfeumo  2530  mo4f  2560  eu3v  2563  eu6  2567  dfeu  2588  eu2  2604  eu4  2610  2mos  2644  2eu4  2649  ceqsex3v  3531  ceqsex4v  3532  ceqsex8v  3534  reu2  3721  reu6  3722  reu4  3727  reu7  3728  rmo3f  3730  rmo4f  3731  2reu5lem3  3753  2reu5  3754  sbcimdv  3851  sbcg  3856  rmo3  3883  reuan  3890  dfpss2  4085  difdif  4130  raldifb  4144  inass  4219  dfss4  4258  dfin2  4260  indi  4273  indifdi  4283  indifdirOLD  4285  undif3  4290  difin0ss  4368  inssdif0  4369  2nreu  4441  2reu4lem  4525  rexdifpr  4661  reuprg0  4706  ssdifsn  4791  ssunpr  4835  uniprg  4925  uniprOLD  4927  uniun  4934  uniin  4935  csbuni  4940  dfiun2g  5033  iunin2  5074  iundif2  5077  iindif2  5080  iinin2  5081  elpwpw  5105  axrep1  5286  axrep4  5290  reusv2lem4  5399  eqvinop  5487  opcom  5501  fconstmpt  5738  opeliunxp  5743  xpundi  5744  elvvv  5751  opelinxp  5755  xpiindi  5835  elcnv2  5877  cnvuni  5886  dmuni  5914  brres  5988  dmres  6003  elidinxp  6043  restidsing  6052  elima3  6066  asymref  6117  imainss  6153  difxp  6163  xpdifid  6167  mptpreima  6237  coundir  6247  resco  6249  coass  6264  relrelss  6272  opreu2reurex  6293  dfpo2  6295  frpoind  6343  wfiOLD  6352  ordtri3or  6396  dffun2  6553  dffun2OLD  6554  dffun2OLDOLD  6555  dffun6  6556  dffun3  6557  dffun3OLD  6558  dffun4  6559  dffun5  6560  dffun6f  6561  dffun7  6575  dffun8  6576  dffun9  6577  svrelfun  6620  fncnv  6621  imadif  6632  dfmpt3  6684  fcnvres  6768  fint  6770  fin  6771  dff12  6786  fores  6815  dff1o4  6841  eqfnfv3  7034  fndmin  7046  fniniseg  7061  unpreima  7064  ffnfvf  7121  fsn2  7136  tpres  7204  fconstfv  7216  dff13f  7258  dff14a  7272  dff14b  7273  isocnv2  7331  f1opr  7468  eloprabga  7519  ffnov  7538  eqfnov  7541  foov  7585  uniuni  7753  tfindsg  7854  findsg  7894  funcnvuni  7926  opabex3d  7956  opabex3rd  7957  opabex3  7958  1stconst  8091  2ndconst  8092  frxp  8117  soxp  8120  xpord3lem  8140  suppvalbr  8155  suppofssd  8194  suppcoss  8198  mpoxopovel  8211  brtpos  8226  tpostpos  8237  dfsmo2  8353  dfrecs3  8378  dfrecs3OLD  8379  rdglem1  8421  tz7.49  8451  brwitnlem  8513  oeeu  8609  naddasslem2  8700  erinxp  8791  mapsncnv  8893  cbvixp  8914  ixpin  8923  ixpiin  8924  mptelixpg  8935  elixpsn  8937  ixpsnf1o  8938  xpassen  9072  omxpenlem  9079  sbthcl  9101  sbthfilem  9207  wemapsolem  9551  dford2  9621  inf2  9624  zfinf  9640  ttrclselem2  9727  trcl  9729  frind  9751  frr3g  9757  iscard2  9977  leweon  10012  aceq1  10118  dfac3  10122  dfac4  10123  dfac5lem2  10125  dfac5  10129  kmlem3  10153  kmlem4  10154  kmlem14  10164  kmlem15  10165  dfackm  10167  infmap2  10219  fin23lem25  10325  zorn2lem7  10503  brdom6disj  10533  zfcndrep  10615  zfcndinf  10619  fpwwe  10647  axgroth4  10833  grothprim  10835  grothtsk  10836  nqpr  11015  addsrmo  11074  mulsrmo  11075  opelreal  11131  elnnz  12575  elznn0nn  12579  peano2uz2  12657  nnwos  12906  dflt2  13134  xmullem  13250  4fvwrd4  13628  preduz  13630  elfznelfzo  13744  fzind2  13757  fsuppmapnn0fiubex  13964  hashinfxadd  14352  hashgt23el  14391  hashfun  14404  fi1uzind  14465  brfi1uzind  14466  opfi1uzind  14469  cotr2g  14930  shftdm  15025  rexfiuz  15301  cbvsum  15648  mertenslem2  15838  mertens  15839  cbvprod  15866  prodmo  15887  iprodmul  15954  divalglem10  16352  ndvdssub  16359  bitsmod  16384  algcvgblem  16521  isprm2  16626  isprm4  16628  hashdvds  16715  infpn2  16853  hashbc0  16945  xpscf  17518  funcpropd  17860  isffth2  17876  eldmcoa  18025  setcinv  18050  xpccatid  18150  yonedainv  18244  ispos  18277  ispos2  18278  joinfval2  18337  meetfval2  18351  istsr2  18547  isnsg2  19079  isnsg4  19090  isgim  19183  oppgid  19271  oppgcntz  19279  symgfix2  19332  efgval2  19640  iscyg2  19798  dmdprdd  19917  subgdmdprd  19952  issrg  20089  oppr1  20248  opprunit  20275  opprirred  20320  isrnghm  20339  isrhm  20376  issubrng  20443  subsubrng2  20460  subsubrg2  20497  rngcinv  20529  ringcinv  20563  islmim  20906  lbsextg  21009  lidlnz  21091  isdomn2  21204  resubdrg  21471  unocv  21543  pjfval2  21574  islinds2  21678  opsrtoslem1  21927  mdetunilem8  22441  istop2g  22718  isbasis2g  22771  tgval2  22779  isclo2  22912  isnrm2  23182  is1stc2  23266  llyi  23298  isfbas2  23659  elfg  23695  ufinffr  23753  isfcls  23833  alexsubALTlem2  23872  alexsubALTlem3  23873  cnextcn  23891  ustfilxp  24037  iscusp2  24127  metustid  24383  isclmp  24944  iscvsp  24975  tcphcph  25085  iscau3  25126  caucfil  25131  mdegleb  25920  ellogdm  26487  dvdsflsumcom  27033  logfac2  27063  dchrelbas3  27084  dchrvmasumlema  27346  nosupno  27549  noinfno  27564  noinfbnd1lem1  27569  dmscut  27657  made0  27713  mulsproplem5  27933  norecdiv  28003  legtrid  28275  outpasch  28439  axcontlem5  28659  axcontlem6  28660  axcontlem7  28661  nb3grpr2  29073  iscplgr  29105  pthdlem1  29456  wwlksnextinj  29586  usgr2wspthon  29652  rusgrnumwwlkl1  29655  isclwwlk  29670  clwwlkccatlem  29675  clwwlknon2x  29789  iseupthf1o  29888  frcond3  29955  frgr3v  29961  4cycl2vnunb  29976  frgrncvvdeqlem2  29986  fusgr2wsp2nb  30020  numclwlk1lem1  30055  hhcms  30889  isch3  30927  ocsh  30969  pjhtheu  31080  pjpreeq  31084  h1deoi  31235  h1dei  31236  eleigvec  31643  cvbr2  31969  cvnbtwn2  31973  cvnbtwn4  31975  mdsl2i  32008  cvmdi  32010  mdsymlem6  32094  cdj3lem3b  32126  mo5f  32162  nmo  32163  rexunirn  32165  dmrab  32170  difrab2  32171  disjunsn  32258  unipreima  32302  dfcnv2  32334  1stpreima  32361  lsmsnorb2  32942  prmidl0  33009  ssmxidl  33030  ressply1mon1p  33097  zarcls  33318  rhmpreimacnlem  33328  isrnsiga  33575  rossros  33642  omsmeas  33786  eulerpartlemr  33837  eulerpartlemgvv  33839  ballotlemodife  33960  plymulx  34023  signstfvneq0  34047  bnj251  34177  bnj252  34178  bnj257  34182  bnj290  34185  bnj1304  34294  bnj153  34355  bnj543  34368  bnj571  34381  bnj580  34388  bnj607  34391  bnj882  34401  bnj964  34418  bnj996  34431  bnj1033  34444  bnj1176  34480  bnj1186  34482  bnj1189  34484  bnj1204  34487  bnj1253  34492  bnj1452  34527  bnj1463  34530  dff15  34551  fineqvrep  34559  fineqvac  34561  lfuhgr3  34574  cusgredgex2  34577  usgrgt2cycl  34585  2cycl2d  34594  dfacycgr1  34599  erdszelem9  34654  cvmlift2lem9  34766  cvmlift2lem13  34770  satfvsucsuc  34820  satfdm  34824  satf0  34827  fmlasucdisj  34854  satffunlem  34856  satffunlem1lem1  34857  satffunlem2lem1  34859  elmthm  35031  axinfprim  35145  axacprim  35146  xpab  35165  dfso2  35195  dford5reg  35224  dfon2lem5  35229  dfon2  35234  brtxp2  35323  brpprod3a  35328  dfom5b  35354  brcart  35374  brimg  35379  funpartlem  35384  dfrecs2  35392  cgrxfr  35497  segletr  35556  trer  35665  fneval  35701  neifg  35720  df3nandALT1  35748  andnand1  35750  nandsym1  35771  bj-eu3f  36184  bj-csbsnlem  36247  bj-snsetex  36308  bj-elsngl  36313  bj-snglc  36314  bj-restuni  36442  bj-dfmpoa  36463  bj-imdirco  36535  mptsnunlem  36683  icorempo  36696  isbasisrelowllem2  36701  relowlpssretop  36709  rdgeqoa  36715  difunieq  36719  dffinxpf  36730  nlpineqsn  36753  curf  36930  finixpnum  36937  ptrest  36951  poimirlem1  36953  poimirlem14  36966  poimirlem16  36968  poimirlem19  36971  poimirlem25  36977  poimirlem26  36978  poimirlem27  36979  poimir  36985  cnambfre  37000  itg2addnc  37006  ftc1anc  37033  opropabco  37056  isdrngo1  37288  keridl  37364  ispridlc  37402  selconj  37432  eldmqsres  37619  cnvepres  37631  ecinn0  37686  alrmomorn  37691  moantr  37697  dfxrn2  37710  disjressuc2  37722  inxpxrn  37729  rnxrnres  37733  coss2cnvepres  37752  refrelredund4  37969  dferALTV2  38002  dfeldisj3  38053  dfpart2  38103  prtlem70  38191  prtlem100  38193  prtlem15  38209  islshpat  38351  lcvbr2  38356  lcvbr3  38357  lcvnbtwn2  38361  ellkr  38423  cvrval2  38608  cvrnbtwn2  38609  cvrnbtwn3  38610  cvrnbtwn4  38613  ishlat2  38687  lplnexatN  38898  islvol5  38914  dath  39071  pclfinclN  39285  lhpexle3  39347  4atex2  39412  4atex2-0bOLDN  39414  isltrn2N  39455  cdleme0nex  39625  cdleme22b  39676  cdlemg17pq  40007  cdlemg19  40019  cdlemg21  40021  cdlemg33d  40044  dibopelvalN  40478  dibopelval2  40480  dib1dim  40500  dicelval2N  40517  diclspsn  40529  lcdlss  40954  mapd1o  40983  3factsumint2  41354  3factsumint3  41355  3factsumint  41357  sticksstones16  41445  sticksstones21  41450  metakunt1  41452  mzpcompact2lem  41952  fz1eqin  41970  rexrabdioph  41995  expdiophlem1  42223  dford4  42231  fnwe2lem2  42256  fgraphopab  42415  dflim6  42477  onsucf1olem  42483  onsucrn  42484  nnoeomeqom  42525  faosnf0.11b  42641  ifpidg  42705  rp-fakeinunass  42729  rp-isfinite6  42732  dfsucon  42737  elinintrab  42791  elnonrel  42799  elmapintab  42810  dfrtrcl5  42843  imaiun1  42865  coiun1  42866  rfovcnvf1od  43218  andi3or  43238  uneqsn  43239  ntrneicls00  43303  rr-groth  43521  ismnushort  43523  rr-grothshortbi  43525  2sbc5g  43638  pm14.12  43643  2sb5nd  43784  uun2221  44037  uun2221p1  44038  uun2221p2  44039  2sb5ndVD  44134  2sb5ndALT  44156  iindif2f  44316  disjinfi  44350  climuz  44919  dfxlim2  45023  cncfshift  45049  dvnmul  45118  dvnprodlem2  45122  ismbl3  45161  ismbl4  45168  stoweidlem26  45201  stoweidlem35  45210  fourierdlem54  45335  fourierdlem83  45364  fourierdlem100  45381  fourierdlem104  45385  fourierdlem109  45390  fourierdlem112  45393  smfpimcc  45983  fcoresf1ob  46242  f1cof1b  46244  f1ocof1ob  46248  2reu8i  46280  dfdfat2  46295  ffnaov  46366  an4com24  46435  4an21  46437  iccpartiltu  46549  prproropf1olem0  46629  2zrngmmgm  47089  rngcinvALTV  47113  ringcinvALTV  47147  opeliun2xp  47171  pgrpgt2nabl  47205  islindeps  47296  lindslinindsimp1  47300  lindslinindsimp2  47306  ldepslinc  47352  blen1b  47436  i0oii  47714  io1ii  47715  iscnrm3lem3  47730  isthinc2  47804  isthinc3  47805  isthincd2  47820  dffun3f  47889  setrec1lem3  47896  elpglem3  47920  elpg  47921