Theorem anim2i 628

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 624	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylanr2  695  abab  839  andi  1023  19.41v  1972  exdistrf  2481  equs45f  2493  moaneu  2653  dariiALT  2695  festinoALT  2704  barocoALT  2706  r19.27v  3194  rspc2ev  3597  reu3  3693  difrab  4273  opthprneg  4825  copsexgwOLD  5463  copsexg  5464  imainss  6142  trssord  6366  ordnbtwn  6445  fof  6782  fv3  6889  fvelimab  6943  dff2  7084  dffo5  7089  foco2  7094  fnsnbOLD  7154  tpres  7189  f13dfv  7262  dff1o6  7263  oprabidw  7431  oprabid  7432  ssoprab2i  7511  ndmovass  7588  ndmovdistr  7589  elovmpt3rab1  7660  tfi  7837  find  7880  releldm2  8028  bropopvvv  8073  bropfvvvvlem  8074  ressuppssdif  8169  omlimcl  8551  odi  8552  ixpf  8906  dif1en  9134  domtrfil  9164  funsnfsupp  9340  hartogs  9494  card2on  9504  zfreg  9546  epfrs  9688  acni3  10019  dfac2b  10102  cflm  10221  axdc2lem  10420  ac6s  10456  ondomon  10535  axregndlem1  10575  axregnd  10577  eltsk2g  10724  grothpw  10799  grothpwex  10800  grothomex  10802  ltexprlem1  11009  ltexprlem4  11012  recexsrlem  11076  elfzp12  13619  hashf1rn  14376  hashdifpr  14440  hashgt23el  14449  hashge2el2dif  14505  ccatsymb  14608  swrdnd0  14683  swrdpfx  14732  pfxpfx  14733  pfxccatin12  14758  cshwidxmod  14828  repswcshw  14837  cshimadifsn  14854  cshimadifsn0  14855  pfxco  14863  wwlktovfo  14983  relexpsucnnl  15055  cau3lem  15394  rlimres  15597  dvdsnegb  16319  dvds2add  16336  dvds2sub  16337  nn0onn  16426  gcd2n0cl  16555  lcmfun  16691  divgcdcoprmex  16712  cncongr1  16713  isfunc  17909  drsdirfi  18349  chnrev  18671  sgrpidmnd  18785  smndex1iidm  18948  gaid  19357  symg2bas  19451  qusecsub  19893  gsumle  20203  c0mgm  20529  rhmisrnghm  20550  c0rhm  20607  rhmsubcrngclem1  20739  srhmsubclem1  20750  abvn0b  20905  lmhmlem  21116  unichnlidl  21328  prmirredlem  21579  psgndiflemB  21707  ismhp  22260  matsubgcell  22548  tposmap  22571  mat1dim0  22587  mat1dimid  22588  mat1dimscm  22589  mat1dimmul  22590  dmatmul  22611  dmatcrng  22616  scmatcrng  22635  scmatf1  22645  1marepvsma1  22697  maducoeval2  22754  smadiadetlem3lem0  22779  slesolinv  22794  cramerimplem1  22797  cramerimplem2  22798  1pmatscmul  22816  cpmatacl  22830  cpmatmcllem  22832  cpmatmcl  22833  mat2pmatf1  22843  mat2pmatghm  22844  mat2pmatmul  22845  mat2pmatlin  22849  mat2pmatscmxcl  22854  m2cpmmhm  22859  m2pmfzgsumcl  22862  decpmatmul  22886  pmatcollpw2lem  22891  monmatcollpw  22893  pmatcollpwfi  22896  pmatcollpw3fi1lem2  22901  pmatcollpwscmatlem1  22903  pmatcollpwscmatlem2  22904  pmatcollpwscmat  22905  pm2mpghm  22930  pm2mpmhmlem2  22933  pm2mp  22939  chmatcl  22942  chmatval  22943  chmaidscmat  22962  chfacfisf  22968  chfacfisfcpmat  22969  chfacfscmulcl  22971  chfacfscmul0  22972  chfacfscmulgsum  22974  chfacfpmmul0  22976  chfacfpmmulgsum  22978  chfacfpmmulgsum2  22979  cayhamlem1  22980  cpmidgsumm2pm  22983  cpmidpmatlem2  22985  cpmadugsumlemB  22988  cpmadugsumlemC  22989  cpmadugsumlemF  22990  cpmadugsumfi  22991  cpmidgsum2  22993  cpmadumatpolylem2  22996  cayhamlem2  22998  chcoeffeqlem  22999  cayleyhamilton0  23003  cayleyhamiltonALT  23005  toponcom  23042  neitr  23294  cnprest  23403  nrmsep2  23470  bwth  23524  2ndcsep  23573  isref  23623  reghaus  23939  isfil2  23970  alexsubALTlem3  24163  cnextcn  24181  lpbl  24617  cmodscmulexp  25238  iscau4  25395  caussi  25413  cmetcusp  25470  ovolicc2lem3  25635  limcresi  26001  elply2  26310  elqaa  26440  aannenlem1  26446  aannenlem2  26447  relogbreexp  26894  cxplogb  26905  bpos1lem  27400  noetalem2  27860  tgjustc1  28698  tgjustc2  28699  axcont  29231  usgrexmplef  29514  subupgr  29542  cplgr3v  29690  cusgrfilem2  29711  usgredgsscusgredg  29714  rusgrprop0  29822  uspgr2wlkeqi  29902  trlontrl  29963  spthonpthon  30005  usgr2wlkspthlem1  30011  usgr2wlkspthlem2  30012  clwlkcompim  30034  clwlkl1loop  30037  wwlksnred  30146  clwwlknonwwlknonb  30362  clwwlknun  30368  1pthon2v  30409  frcond1  30522  frcond4  30526  frgrnbnb  30549  clwlknon2num  30624  numclwlk1lem1  30625  numclwlk1lem2  30626  numclwwlkovh  30629  numclwwlk2lem1  30632  numclwlk2lem2f  30633  numclwwlk2  30637  isgrpo  30754  vcz  30832  hvsub4  31294  hvaddsub4  31335  5oalem2  31912  5oalem5  31915  5oalem6  31916  3oalem2  31920  homcl  32003  hoadddi  32060  stle0i  32496  spansncv2  32550  mdsymlem1  32660  cdj3lem1  32691  f1ocnt  33053  gsumvsca1  33454  gsumvsca2  33455  crefdf  34150  sxbrsigalem0  34573  dya2icoseg2  34580  eulerpartlemgvv  34678  ballotlemirc  34834  bnj168  35031  bnj546  35196  bnj594  35212  bnj1097  35281  bnj1110  35282  bnj1174  35303  bnj1176  35305  axprALT2  35412  cusgredgex2  35481  acycgrislfgr  35510  umgracycusgr  35512  cusgracyclt3v  35514  satfv1  35721  satf0suclem  35733  fmlasuc0  35742  fmlafvel  35743  satffunlem2lem1  35762  satfun  35769  fv1stcnv  36135  colineardim1  36419  idinside  36442  finminlem  36686  ivthALT  36703  lukshef-ax2  36783  regsfromregtco  36906  bj-19.41al  37138  bj-equs45fv  37303  bj-elabd2ALT  37417  bj-rest10b  37586  copsex2b  37639  bj-elid6  37669  bj-ccinftydisj  37712  mptsnunlem  37839  topdifinffinlem  37848  relowlssretop  37864  elxp8  37872  fvineqsnf1  37911  pibt1  37917  matunitlindflem1  38122  poimirlem22  38148  poimirlem25  38151  poimirlem27  38153  poimirlem31  38157  ovoliunnfl  38168  itg2addnclem  38177  sstotbnd3  38282  heibor1lem  38315  heibor1  38316  rngmgmbs4  38437  exmid2  38605  redundss3  39218  redundpim3  39220  dalem53  40356  dalem54  40357  linepsubN  40383  pmapsub  40399  elpaddri  40433  pclfinN  40531  pclcmpatN  40532  cdlemg33c0  41333  dihatexv2  41970  eldioph4i  43396  acongtr  43562  pwfi2f1o  43680  aaitgo  43746  tfsconcat0b  43930  frege54cor0a  44446  clsf2  44709  ismnushort  44870  dvsconst  44899  mptssid  45815  xlimxrre  46404  icccncfext  46460  dvmptfprod  46518  stoweidlem17  46590  elaa2  46807  dmfcoafv  47768  elfzelfzlble  47914  prprelprb  48122  fmtnoprmfac1  48173  fmtnoprmfac2  48175  flsqrt  48201  lighneallem3  48215  proththd  48222  evenprm2  48335  gbogbow  48377  clnbgrel  48449  clnbgredg  48461  uhgrimisgrgric  48552  isubgr3stgrlem1  48587  isubgr3stgr  48596  gpg3nbgrvtx0  48697  gpgvtxdg3  48703  2zrngnmrid  48877  rhmsubcALTVlem3  48904  linccl  49046  lincvalpr  49050  lincdifsn  49056  lincext1  49086  lindslinindsimp1  49089  ldepspr  49105  lincresunit3lem1  49111  logblt1b  49196  dignnld  49235  dig1  49240  dignn0flhalflem1  49247  itcovalsucov  49300  line  49364  rrxline  49366  rrxsphere  49380  itschlc0xyqsol1  49398  itsclc0xyqsolr  49401  lubeldm2  49586  glbeldm2  49587  isinito4a  50178  amgmwlem  50432