Theorem anim2i 610

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim2i	⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 606	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  sylanl2  671  sylanr2  673  andi  993  19.41v  1992  sbimi  2017  exdistrf  2413  equs45f  2425  moaneu  2659  dariiALT  2698  festinoALT  2709  barocoALT  2711  r19.27v  3256  rspc2ev  3526  reu3  3608  difrab  4127  opthprneg  4628  copsexg  5187  imainss  5802  trssord  5993  ordnbtwn  6066  fof  6366  fv3  6464  fvelimab  6513  dff2  6635  dffo5  6640  foco2  6643  fnsnb  6699  tpres  6738  f13dfv  6802  dff1o6  6803  oprabid  6953  ssoprab2i  7026  ndmovass  7099  ndmovdistr  7100  elovmpt3rab1  7170  tfi  7331  find  7369  releldm2  7497  bropopvvv  7536  bropfvvvvlem  7537  ressuppssdif  7597  supp0cosupp0  7616  imacosupp  7617  omlimcl  7942  odi  7943  ixpf  8216  funsnfsupp  8587  hartogs  8738  card2on  8748  zfreg  8789  epfrs  8904  acni3  9203  dfac2b  9286  dfac2OLD  9288  cflm  9407  axdc2lem  9605  ac6s  9641  ondomon  9720  axregndlem1  9759  axregnd  9761  eltsk2g  9908  grothpw  9983  grothpwex  9984  grothomex  9986  ltexprlem1  10193  ltexprlem4  10196  recexsrlem  10260  elfzp12  12737  focdmex  13456  hashf1rn  13458  hashdifpr  13517  hashge2el2dif  13576  ccatsymb  13672  swrdnd0  13752  swrdpfx  13818  pfxpfx  13820  swrdccatin2  13856  swrdccatin12lem2OLD  13859  pfxccatin12  13861  swrdccatin12OLD  13862  splvalpfxOLD  13889  repswpfx  13931  cshwidxmod  13954  repswcshw  13963  cshimadifsn  13980  cshimadifsn0  13981  pfxco  13989  wwlktovfo  14110  relexpsucnnl  14179  cau3lem  14501  rlimres  14697  dvdsnegb  15406  dvds2add  15422  dvds2sub  15423  nn0onn  15510  gcd2n0cl  15637  lcmfun  15764  divgcdcoprmex  15785  cncongr1  15786  isfunc  16909  drsdirfi  17324  gimcnv  18093  gaid  18115  symg2bas  18201  gsummptnn0fz  18768  gsummptnn0fzOLD  18769  lmhmlem  19424  lmimcnv  19462  abvn0b  19699  prmirredlem  20237  psgndiflemB  20342  matbas2  20631  matsubgcell  20644  tposmap  20668  mat1dim0  20684  mat1dimid  20685  mat1dimscm  20686  mat1dimmul  20687  dmatmul  20708  dmatcrng  20713  scmatcrng  20732  scmatf1  20742  1marepvsma1  20794  maducoeval2  20851  smadiadetlem3lem0  20877  slesolinv  20892  cramerimplem1  20895  cramerimplem1OLD  20896  cramerimplem2  20897  1pmatscmul  20914  cpmatacl  20928  cpmatmcllem  20930  cpmatmcl  20931  mat2pmatf1  20941  mat2pmatghm  20942  mat2pmatmul  20943  mat2pmatlin  20947  mat2pmatscmxcl  20952  m2cpmmhm  20957  m2pmfzgsumcl  20960  m2cpmrngiso  20970  decpmatmul  20984  pmatcollpw2lem  20989  monmatcollpw  20991  pmatcollpwfi  20994  pmatcollpw3fi1lem2  20999  pmatcollpwscmatlem1  21001  pmatcollpwscmatlem2  21002  pmatcollpwscmat  21003  pm2mpghm  21028  pm2mpmhmlem2  21031  pm2mp  21037  chmatcl  21040  chmatval  21041  chmaidscmat  21060  chfacfisf  21066  chfacfisfcpmat  21067  chfacfscmulcl  21069  chfacfscmul0  21070  chfacfscmulgsum  21072  chfacfpmmul0  21074  chfacfpmmulgsum  21076  chfacfpmmulgsum2  21077  cayhamlem1  21078  cpmidgsumm2pm  21081  cpmidpmatlem2  21083  cpmadugsumlemB  21086  cpmadugsumlemC  21087  cpmadugsumlemF  21088  cpmadugsumfi  21089  cpmidgsum2  21091  cpmadumatpolylem2  21094  cayhamlem2  21096  chcoeffeqlem  21097  cayleyhamilton0  21101  cayleyhamiltonALT  21103  toprntopon  21137  toponcom  21140  neitr  21392  cnprest  21501  nrmsep2  21568  bwth  21622  2ndcsep  21671  isref  21721  reghaus  22037  isfil2  22068  alexsubALTlem3  22261  cnextcn  22279  lpbl  22716  cmodscmulexp  23329  iscau4  23485  caussi  23503  cmetcusp  23560  ovolicc2lem3  23723  limcresi  24086  elply2  24389  elqaa  24514  aannenlem1  24520  aannenlem2  24521  relogbreexp  24953  cxplogb  24964  bpos1lem  25459  tgjustc1  25826  tgjustc2  25827  axcont  26325  usgrexmplef  26606  subupgr  26634  cplgr3v  26783  cusgrfilem2  26804  usgredgsscusgredg  26807  rusgrprop0  26915  uspgr2wlkeqi  26995  spthonpthon  27103  usgr2wlkspthlem1  27109  usgr2wlkspthlem2  27110  usgr2trlncl  27112  clwlkcompim  27132  clwlkl1loop  27135  wlkwwlkinjOLD  27247  wwlksnred  27252  wwlksnredOLD  27253  wwlksnextbiOLD  27256  wwlksnfiOLD  27279  clwwlkccat  27370  clwwlknonwwlknonb  27508  clwwlknun  27514  1pthon2v  27556  frcond1  27674  frcond4  27678  frgrnbnb  27701  clwlknon2num  27796  numclwlk1lem1  27797  numclwlk1lem2  27798  numclwwlkovh  27801  numclwwlk2lem1  27804  numclwlk2lem2f  27805  numclwlk2lem2fOLD  27808  numclwwlk2  27813  frgrregord013  27827  isgrpo  27924  vcz  28002  hvsub4  28466  hvaddsub4  28507  5oalem2  29086  5oalem5  29089  5oalem6  29090  3oalem2  29094  homcl  29177  hoadddi  29234  stle0i  29670  spansncv2  29724  mdsymlem1  29834  cdj3lem1  29865  disjin  29962  disjin2  29963  f1ocnt  30123  gsumle  30341  gsumvsca1  30344  gsumvsca2  30345  pmtrprfv2  30446  crefdf  30513  sxbrsigalem0  30931  dya2icoseg2  30938  eulerpartlemgvv  31036  ballotlemirc  31192  bnj168  31398  bnj546  31565  bnj594  31581  bnj1097  31648  bnj1110  31649  bnj1174  31670  bnj1176  31672  fv1stcnv  32268  noetalem5  32456  colineardim1  32757  idinside  32780  finminlem  32901  ivthALT  32918  lukshef-ax2  32997  bj-19.41al  33227  bj-equs45fv  33337  bj-rest10b  33615  bj-ccinftydisj  33690  mptsnunlem  33781  topdifinffinlem  33790  relowlssretop  33806  elxp8  33814  matunitlindflem1  34031  poimirlem22  34057  poimirlem25  34060  poimirlem27  34062  poimirlem31  34066  ovoliunnfl  34077  itg2addnclem  34086  indexa  34153  sstotbnd3  34199  heibor1lem  34232  heibor1  34233  rngmgmbs4  34354  exmid2  34524  redss3  34997  redpim3  34999  dalem53  35879  dalem54  35880  linepsubN  35906  pmapsub  35922  elpaddri  35956  pclfinN  36054  pclcmpatN  36055  cdlemg33c0  36856  dihatexv2  37493  eldioph4i  38336  acongtr  38504  pwfi2f1o  38625  aaitgo  38691  frege54cor0a  39113  clsf2  39380  dvsconst  39485  xlimxrre  40971  icccncfext  41028  stoweidlem17  41161  elaa2  41378  fundmdfat  42170  dmfcoafv  42216  elfzelfzlble  42363  prprelprb  42456  fmtnoprmfac1  42498  fmtnoprmfac2  42500  flsqrt  42529  lighneallem3  42545  proththd  42552  evenprm2  42648  gbogbow  42669  uspgrsprfo  42771  c0mgm  42924  c0rhm  42927  rhmisrnghm  42935  lidlmmgm  42940  2zrngnmrid  42965  rhmsubcrngclem1  43042  srhmsubclem1  43088  rhmsubcALTVlem3  43121  linccl  43218  lincvalpr  43222  lincdifsn  43228  lincext1  43258  lindslinindsimp1  43261  ldepspr  43277  lincresunit3lem1  43283  logblt1b  43373  dignnld  43412  dig1  43417  dignn0flhalflem1  43424  line  43468  rrxline  43470  rrxsphere  43484  itschlc0xyqsol1  43502  itsclc0xyqsolr  43505  amgmwlem  43654