Theorem anim2i 629

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanr2  696  abab  840  andi  1025  19.41v  1982  exdistrf  2482  equs45f  2494  moaneu  2654  dariiALT  2696  festinoALT  2705  barocoALT  2707  r19.27v  3197  rspc2ev  3597  reu3  3693  difrab  4274  opthprneg  4835  copsexgwOLD  5478  copsexg  5479  imainss  6156  trssord  6384  ordnbtwn  6463  fof  6799  fv3  6906  fvelimab  6960  dff2  7101  dffo5  7106  foco2  7111  fnsnbOLD  7171  tpres  7206  f13dfv  7283  dff1o6  7284  oprabidw  7454  oprabid  7455  ssoprab2i  7534  ndmovass  7611  ndmovdistr  7612  elovmpt3rab1  7683  tfi  7858  find  7901  releldm2  8049  bropopvvv  8094  bropfvvvvlem  8095  ressuppssdif  8190  omlimcl  8572  odi  8573  ixpf  8927  dif1en  9156  domtrfil  9186  funsnfsupp  9362  hartogs  9516  card2on  9526  zfreg  9568  epfrs  9710  acni3  10050  dfac2b  10133  cflm  10251  axdc2lem  10450  ac6s  10486  ondomon  10565  axregndlem1  10605  axregnd  10607  eltsk2g  10754  grothpw  10829  grothpwex  10830  grothomex  10832  ltexprlem1  11039  ltexprlem4  11042  recexsrlem  11106  elfzp12  13650  hashf1rn  14408  hashdifpr  14472  hashgt23el  14481  hashge2el2dif  14537  ccatsymb  14640  swrdnd0  14719  swrdpfx  14768  pfxpfx  14769  pfxccatin12  14794  cshwidxmod  14866  repswcshw  14875  cshimadifsn  14892  cshimadifsn0  14893  pfxco  14901  wwlktovfo  15021  relexpsucnnl  15093  cau3lem  15432  rlimres  15635  dvdsnegb  16356  dvds2add  16373  dvds2sub  16374  nn0onn  16463  gcd2n0cl  16592  lcmfun  16728  divgcdcoprmex  16749  cncongr1  16750  isfunc  17946  drsdirfi  18386  chnrev  18708  sgrpidmnd  18826  smndex1iidm  18991  gaid  19400  symg2bas  19494  qusecsub  19936  gsumle  20246  c0mgm  20574  rhmisrnghm  20596  c0rhm  20670  rhmsubcrngclem1  20802  srhmsubclem1  20813  abvn0b  20976  lmhmlem  21187  unichnlidl  21399  prmirredlem  21659  psgndiflemB  21787  ismhp  22340  matsubgcell  22628  tposmap  22651  mat1dim0  22667  mat1dimid  22668  mat1dimscm  22669  mat1dimmul  22670  dmatmul  22691  dmatcrng  22696  scmatcrng  22715  scmatf1  22725  1marepvsma1  22777  maducoeval2  22834  smadiadetlem3lem0  22859  slesolinv  22874  cramerimplem1  22877  cramerimplem2  22878  1pmatscmul  22896  cpmatacl  22910  cpmatmcllem  22912  cpmatmcl  22913  mat2pmatf1  22923  mat2pmatghm  22924  mat2pmatmul  22925  mat2pmatlin  22929  mat2pmatscmxcl  22934  m2cpmmhm  22939  m2pmfzgsumcl  22942  decpmatmul  22966  pmatcollpw2lem  22971  monmatcollpw  22973  pmatcollpwfi  22976  pmatcollpw3fi1lem2  22981  pmatcollpwscmatlem1  22983  pmatcollpwscmatlem2  22984  pmatcollpwscmat  22985  pm2mpghm  23010  pm2mpmhmlem2  23013  pm2mp  23019  chmatcl  23022  chmatval  23023  chmaidscmat  23042  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulcl  23051  chfacfscmul0  23052  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulgsum  23058  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmidgsumm2pm  23063  cpmidpmatlem2  23065  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  cpmadugsumfi  23071  cpmidgsum2  23073  cpmadumatpolylem2  23076  cayhamlem2  23078  chcoeffeqlem  23079  cayleyhamilton0  23083  cayleyhamiltonALT  23085  toponcom  23122  neitr  23374  cnprest  23483  nrmsep2  23550  bwth  23604  2ndcsep  23653  isref  23703  reghaus  24019  isfil2  24050  alexsubALTlem3  24243  cnextcn  24261  lpbl  24697  cmodscmulexp  25318  iscau4  25475  caussi  25493  cmetcusp  25550  ovolicc2lem3  25715  limcresi  26081  elply2  26390  elqaa  26520  aannenlem1  26528  aannenlem2  26529  relogbreexp  26977  cxplogb  26988  bpos1lem  27483  noetalem2  27943  tgjustc1  28781  tgjustc2  28782  axcont  29363  usgrexmplef  29646  subupgr  29674  cplgr3v  29822  cusgrfilem2  29843  usgredgsscusgredg  29846  rusgrprop0  29954  uspgr2wlkeqi  30034  trlontrl  30095  spthonpthon  30137  usgr2wlkspthlem1  30143  usgr2wlkspthlem2  30144  clwlkcompim  30166  clwlkl1loop  30169  wwlksnred  30278  clwwlknonwwlknonb  30494  clwwlknun  30500  1pthon2v  30541  frcond1  30654  frcond4  30658  frgrnbnb  30681  clwlknon2num  30756  numclwlk1lem1  30757  numclwlk1lem2  30758  numclwwlkovh  30761  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwwlk2  30769  isgrpo  30886  vcz  30964  hvsub4  31426  hvaddsub4  31467  5oalem2  32044  5oalem5  32047  5oalem6  32048  3oalem2  32052  homcl  32135  hoadddi  32192  stle0i  32628  spansncv2  32682  mdsymlem1  32792  cdj3lem1  32823  f1ocnt  33182  gsumvsca1  33577  gsumvsca2  33578  crefdf  34269  sxbrsigalem0  34693  dya2icoseg2  34700  eulerpartlemgvv  34798  ballotlemirc  34954  bnj168  35151  bnj546  35316  bnj594  35332  bnj1097  35401  bnj1110  35402  bnj1174  35423  bnj1176  35425  axprALT2  35528  cusgredgex2  35636  acycgrislfgr  35665  umgracycusgr  35667  cusgracyclt3v  35669  satfv1  35876  satf0suclem  35888  fmlasuc0  35897  fmlafvel  35898  satffunlem2lem1  35917  satfun  35924  fv1stcnv  36290  colineardim1  36574  idinside  36597  finminlem  36870  ivthALT  36887  lukshef-ax2  36967  regsfromregtco  37090  bj-19.41al  37322  bj-equs45fv  37487  bj-elabd2ALT  37602  bj-rest10b  37772  copsex2b  37825  bj-elid6  37855  bj-ccinftydisj  37898  mptsnunlem  38025  topdifinffinlem  38034  relowlssretop  38050  elxp8  38058  fvineqsnf1  38097  pibt1  38103  matunitlindflem1  38308  poimirlem22  38334  poimirlem25  38337  poimirlem27  38339  poimirlem31  38343  ovoliunnfl  38354  itg2addnclem  38363  sstotbnd3  38468  heibor1lem  38501  heibor1  38502  rngmgmbs4  38623  exmid2  38789  redundss3  39402  redundpim3  39404  dalem53  40540  dalem54  40541  linepsubN  40567  pmapsub  40583  elpaddri  40617  pclfinN  40715  pclcmpatN  40716  cdlemg33c0  41517  dihatexv2  42154  eldioph4i  43580  acongtr  43746  pwfi2f1o  43864  aaitgo  43930  tfsconcat0b  44114  frege54cor0a  44630  clsf2  44893  ismnushort  45052  dvsconst  45081  mptssid  45997  xlimxrre  46586  icccncfext  46642  dvmptfprod  46700  stoweidlem17  46772  elaa2  46989  dmfcoafv  47953  elfzelfzlble  48099  prprelprb  48307  fmtnoprmfac1  48358  fmtnoprmfac2  48360  flsqrt  48386  lighneallem3  48400  proththd  48407  evenprm2  48520  gbogbow  48562  clnbgrel  48634  clnbgredg  48646  uhgrimisgrgric  48737  isubgr3stgrlem1  48772  isubgr3stgr  48781  gpg3nbgrvtx0  48882  gpgvtxdg3  48888  2zrngnmrid  49062  rhmsubcALTVlem3  49089  linccl  49235  lincvalpr  49239  lincdifsn  49245  lincext1  49275  lindslinindsimp1  49278  ldepspr  49294  lincresunit3lem1  49300  logblt1b  49385  dignnld  49424  dig1  49429  dignn0flhalflem1  49436  itcovalsucov  49489  line  49553  rrxline  49555  rrxsphere  49569  itschlc0xyqsol1  49587  itsclc0xyqsolr  49590  lubeldm2  49775  glbeldm2  49776  isinito4a  50367  alseuals  50643  ralseurals  50644  amgmwlem  50691