Theorem anim2i 616

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

Syntax hints:   → wi 4   ∧ 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:  sylanr2  679  andi  1004  19.41v  1954  exdistrf  2447  equs45f  2459  moaneu  2625  dariiALT  2667  festinoALT  2676  barocoALT  2678  r19.27v  3109  rspc2ev  3564  reu3  3657  difrab  4239  opthprneg  4792  copsexgw  5398  copsexg  5399  imainss  6046  trssord  6268  ordnbtwn  6341  fof  6672  fv3  6774  fvelimab  6823  dff2  6957  dffo5  6962  foco2  6965  fnsnb  7020  tpres  7058  f13dfv  7127  dff1o6  7128  oprabidw  7286  oprabid  7287  ssoprab2i  7363  ndmovass  7438  ndmovdistr  7439  elovmpt3rab1  7507  tfi  7675  find  7717  findOLD  7718  releldm2  7857  bropopvvv  7901  bropfvvvvlem  7902  ressuppssdif  7972  omlimcl  8371  odi  8372  ixpf  8666  funsnfsupp  9082  hartogs  9233  card2on  9243  zfreg  9284  epfrs  9420  acni3  9734  dfac2b  9817  cflm  9937  axdc2lem  10135  ac6s  10171  ondomon  10250  axregndlem1  10289  axregnd  10291  eltsk2g  10438  grothpw  10513  grothpwex  10514  grothomex  10516  ltexprlem1  10723  ltexprlem4  10726  recexsrlem  10790  elfzp12  13264  focdmex  13993  hashf1rn  13995  hashdifpr  14058  hashgt23el  14067  hashge2el2dif  14122  ccatsymb  14215  swrdnd0  14298  swrdpfx  14348  pfxpfx  14349  pfxccatin12  14374  cshwidxmod  14444  repswcshw  14453  cshimadifsn  14470  cshimadifsn0  14471  pfxco  14479  wwlktovfo  14601  relexpsucnnl  14669  cau3lem  14994  rlimres  15195  dvdsnegb  15911  dvds2add  15927  dvds2sub  15928  nn0onn  16017  gcd2n0cl  16144  lcmfun  16278  divgcdcoprmex  16299  cncongr1  16300  isfunc  17495  drsdirfi  17938  sgrpidmnd  18305  smndex1iidm  18455  gaid  18820  symg2bas  18915  lmhmlem  20206  abvn0b  20486  prmirredlem  20606  psgndiflemB  20717  matsubgcell  21491  tposmap  21514  mat1dim0  21530  mat1dimid  21531  mat1dimscm  21532  mat1dimmul  21533  dmatmul  21554  dmatcrng  21559  scmatcrng  21578  scmatf1  21588  1marepvsma1  21640  maducoeval2  21697  smadiadetlem3lem0  21722  slesolinv  21737  cramerimplem1  21740  cramerimplem2  21741  1pmatscmul  21759  cpmatacl  21773  cpmatmcllem  21775  cpmatmcl  21776  mat2pmatf1  21786  mat2pmatghm  21787  mat2pmatmul  21788  mat2pmatlin  21792  mat2pmatscmxcl  21797  m2cpmmhm  21802  m2pmfzgsumcl  21805  m2cpmrngiso  21815  decpmatmul  21829  pmatcollpw2lem  21834  monmatcollpw  21836  pmatcollpwfi  21839  pmatcollpw3fi1lem2  21844  pmatcollpwscmatlem1  21846  pmatcollpwscmatlem2  21847  pmatcollpwscmat  21848  pm2mpghm  21873  pm2mpmhmlem2  21876  pm2mp  21882  chmatcl  21885  chmatval  21886  chmaidscmat  21905  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmulcl  21914  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmidgsumm2pm  21926  cpmidpmatlem2  21928  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmidgsum2  21936  cpmadumatpolylem2  21939  cayhamlem2  21941  chcoeffeqlem  21942  cayleyhamilton0  21946  cayleyhamiltonALT  21948  toponcom  21985  neitr  22239  cnprest  22348  nrmsep2  22415  bwth  22469  2ndcsep  22518  isref  22568  reghaus  22884  isfil2  22915  alexsubALTlem3  23108  cnextcn  23126  lpbl  23565  cmodscmulexp  24191  iscau4  24348  caussi  24366  cmetcusp  24423  ovolicc2lem3  24588  limcresi  24954  elply2  25262  elqaa  25387  aannenlem1  25393  aannenlem2  25394  relogbreexp  25830  cxplogb  25841  bpos1lem  26335  tgjustc1  26740  tgjustc2  26741  axcont  27247  usgrexmplef  27529  subupgr  27557  cplgr3v  27705  cusgrfilem2  27726  usgredgsscusgredg  27729  rusgrprop0  27837  uspgr2wlkeqi  27917  trlontrl  27980  spthonpthon  28020  usgr2wlkspthlem1  28026  usgr2wlkspthlem2  28027  clwlkcompim  28049  clwlkl1loop  28052  wwlksnred  28158  clwwlknonwwlknonb  28371  clwwlknun  28377  1pthon2v  28418  frcond1  28531  frcond4  28535  frgrnbnb  28558  clwlknon2num  28633  numclwlk1lem1  28634  numclwlk1lem2  28635  numclwwlkovh  28638  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwwlk2  28646  isgrpo  28760  vcz  28838  hvsub4  29300  hvaddsub4  29341  5oalem2  29918  5oalem5  29921  5oalem6  29922  3oalem2  29926  homcl  30009  hoadddi  30066  stle0i  30502  spansncv2  30556  mdsymlem1  30666  cdj3lem1  30697  f1ocnt  31025  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  crefdf  31700  sxbrsigalem0  32138  dya2icoseg2  32145  eulerpartlemgvv  32243  ballotlemirc  32398  bnj168  32609  bnj546  32776  bnj594  32792  bnj1097  32861  bnj1110  32862  bnj1174  32883  bnj1176  32885  cusgredgex2  32984  acycgrislfgr  33014  umgracycusgr  33016  cusgracyclt3v  33018  satfv1  33225  satf0suclem  33237  fmlasuc0  33246  fmlafvel  33247  satffunlem2lem1  33266  satfun  33273  fv1stcnv  33657  noetalem2  33872  colineardim1  34290  idinside  34313  finminlem  34434  ivthALT  34451  lukshef-ax2  34531  bj-19.41al  34767  bj-equs45fv  34920  bj-elabd2ALT  35040  bj-rest10b  35187  copsex2b  35238  bj-elid6  35268  bj-ccinftydisj  35311  mptsnunlem  35436  topdifinffinlem  35445  relowlssretop  35461  elxp8  35469  fvineqsnf1  35508  pibt1  35514  matunitlindflem1  35700  poimirlem22  35726  poimirlem25  35729  poimirlem27  35731  poimirlem31  35735  ovoliunnfl  35746  itg2addnclem  35755  sstotbnd3  35861  heibor1lem  35894  heibor1  35895  rngmgmbs4  36016  exmid2  36184  redundss3  36668  redundpim3  36670  dalem53  37666  dalem54  37667  linepsubN  37693  pmapsub  37709  elpaddri  37743  pclfinN  37841  pclcmpatN  37842  cdlemg33c0  38643  dihatexv2  39280  eldioph4i  40550  acongtr  40716  pwfi2f1o  40837  aaitgo  40903  frege54cor0a  41360  clsf2  41625  ismnushort  41808  dvsconst  41837  mptssid  42674  xlimxrre  43262  icccncfext  43318  stoweidlem17  43448  elaa2  43665  dmfcoafv  44554  elfzelfzlble  44701  prprelprb  44857  fmtnoprmfac1  44905  fmtnoprmfac2  44907  flsqrt  44933  lighneallem3  44947  proththd  44954  evenprm2  45054  gbogbow  45096  c0mgm  45355  c0rhm  45358  rhmisrnghm  45366  lidlmmgm  45371  2zrngnmrid  45396  rhmsubcrngclem1  45473  srhmsubclem1  45519  rhmsubcALTVlem3  45552  linccl  45643  lincvalpr  45647  lincdifsn  45653  lincext1  45683  lindslinindsimp1  45686  ldepspr  45702  lincresunit3lem1  45708  logblt1b  45798  dignnld  45837  dig1  45842  dignn0flhalflem1  45849  itcovalsucov  45902  line  45966  rrxline  45968  rrxsphere  45982  itschlc0xyqsol1  46000  itsclc0xyqsolr  46003  lubeldm2  46138  glbeldm2  46139  amgmwlem  46392