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  680  andi  1005  19.41v  1952  exdistrf  2445  equs45f  2457  moaneu  2618  dariiALT  2660  festinoALT  2669  barocoALT  2671  r19.27v  3186  rspc2ev  3624  reu3  3723  difrab  4308  opthprneg  4865  copsexgw  5490  copsexg  5491  imainss  6153  trssord  6381  ordnbtwn  6457  fof  6805  fv3  6909  fvelimab  6964  dff2  7100  dffo5  7105  foco2  7110  fnsnb  7166  tpres  7204  f13dfv  7275  dff1o6  7276  oprabidw  7443  oprabid  7444  ssoprab2i  7522  ndmovass  7599  ndmovdistr  7600  elovmpt3rab1  7670  tfi  7846  find  7891  findOLD  7892  releldm2  8033  bropopvvv  8081  bropfvvvvlem  8082  ressuppssdif  8175  omlimcl  8584  odi  8585  ixpf  8920  dif1en  9166  domtrfil  9201  funsnfsupp  9393  hartogs  9545  card2on  9555  zfreg  9596  epfrs  9732  acni3  10048  dfac2b  10131  cflm  10251  axdc2lem  10449  ac6s  10485  ondomon  10564  axregndlem1  10603  axregnd  10605  eltsk2g  10752  grothpw  10827  grothpwex  10828  grothomex  10830  ltexprlem1  11037  ltexprlem4  11040  recexsrlem  11104  elfzp12  13587  hashf1rn  14319  hashdifpr  14382  hashgt23el  14391  hashge2el2dif  14448  ccatsymb  14539  swrdnd0  14614  swrdpfx  14664  pfxpfx  14665  pfxccatin12  14690  cshwidxmod  14760  repswcshw  14769  cshimadifsn  14787  cshimadifsn0  14788  pfxco  14796  wwlktovfo  14916  relexpsucnnl  14984  cau3lem  15308  rlimres  15509  dvdsnegb  16224  dvds2add  16240  dvds2sub  16241  nn0onn  16330  gcd2n0cl  16457  lcmfun  16589  divgcdcoprmex  16610  cncongr1  16611  isfunc  17821  drsdirfi  18268  sgrpidmnd  18670  smndex1iidm  18824  gaid  19211  symg2bas  19308  qusecsub  19751  c0mgm  20357  rhmisrnghm  20378  c0rhm  20430  rhmsubcrngclem1  20558  srhmsubclem1  20569  lmhmlem  20873  abvn0b  21210  prmirredlem  21333  psgndiflemB  21464  matsubgcell  22257  tposmap  22280  mat1dim0  22296  mat1dimid  22297  mat1dimscm  22298  mat1dimmul  22299  dmatmul  22320  dmatcrng  22325  scmatcrng  22344  scmatf1  22354  1marepvsma1  22406  maducoeval2  22463  smadiadetlem3lem0  22488  slesolinv  22503  cramerimplem1  22506  cramerimplem2  22507  1pmatscmul  22525  cpmatacl  22539  cpmatmcllem  22541  cpmatmcl  22542  mat2pmatf1  22552  mat2pmatghm  22553  mat2pmatmul  22554  mat2pmatlin  22558  mat2pmatscmxcl  22563  m2cpmmhm  22568  m2pmfzgsumcl  22571  decpmatmul  22595  pmatcollpw2lem  22600  monmatcollpw  22602  pmatcollpwfi  22605  pmatcollpw3fi1lem2  22610  pmatcollpwscmatlem1  22612  pmatcollpwscmatlem2  22613  pmatcollpwscmat  22614  pm2mpghm  22639  pm2mpmhmlem2  22642  pm2mp  22648  chmatcl  22651  chmatval  22652  chmaidscmat  22671  chfacfisf  22677  chfacfisfcpmat  22678  chfacfscmulcl  22680  chfacfscmul0  22681  chfacfscmulgsum  22683  chfacfpmmul0  22685  chfacfpmmulgsum  22687  chfacfpmmulgsum2  22688  cayhamlem1  22689  cpmidgsumm2pm  22692  cpmidpmatlem2  22694  cpmadugsumlemB  22697  cpmadugsumlemC  22698  cpmadugsumlemF  22699  cpmadugsumfi  22700  cpmidgsum2  22702  cpmadumatpolylem2  22705  cayhamlem2  22707  chcoeffeqlem  22708  cayleyhamilton0  22712  cayleyhamiltonALT  22714  toponcom  22751  neitr  23005  cnprest  23114  nrmsep2  23181  bwth  23235  2ndcsep  23284  isref  23334  reghaus  23650  isfil2  23681  alexsubALTlem3  23874  cnextcn  23892  lpbl  24333  cmodscmulexp  24970  iscau4  25128  caussi  25146  cmetcusp  25203  ovolicc2lem3  25369  limcresi  25735  elply2  26049  elqaa  26175  aannenlem1  26181  aannenlem2  26182  relogbreexp  26622  cxplogb  26633  bpos1lem  27130  noetalem2  27590  tgjustc1  28161  tgjustc2  28162  axcont  28669  usgrexmplef  28951  subupgr  28979  cplgr3v  29127  cusgrfilem2  29148  usgredgsscusgredg  29151  rusgrprop0  29259  uspgr2wlkeqi  29340  trlontrl  29403  spthonpthon  29443  usgr2wlkspthlem1  29449  usgr2wlkspthlem2  29450  clwlkcompim  29472  clwlkl1loop  29475  wwlksnred  29581  clwwlknonwwlknonb  29794  clwwlknun  29800  1pthon2v  29841  frcond1  29954  frcond4  29958  frgrnbnb  29981  clwlknon2num  30056  numclwlk1lem1  30057  numclwlk1lem2  30058  numclwwlkovh  30061  numclwwlk2lem1  30064  numclwlk2lem2f  30065  numclwwlk2  30069  isgrpo  30185  vcz  30263  hvsub4  30725  hvaddsub4  30766  5oalem2  31343  5oalem5  31346  5oalem6  31347  3oalem2  31351  homcl  31434  hoadddi  31491  stle0i  31927  spansncv2  31981  mdsymlem1  32091  cdj3lem1  32122  f1ocnt  32448  gsumle  32680  gsumvsca1  32809  gsumvsca2  32810  crefdf  33294  sxbrsigalem0  33736  dya2icoseg2  33743  eulerpartlemgvv  33841  ballotlemirc  33996  bnj168  34207  bnj546  34373  bnj594  34389  bnj1097  34458  bnj1110  34459  bnj1174  34480  bnj1176  34482  cusgredgex2  34579  acycgrislfgr  34609  umgracycusgr  34611  cusgracyclt3v  34613  satfv1  34820  satf0suclem  34832  fmlasuc0  34841  fmlafvel  34842  satffunlem2lem1  34861  satfun  34868  fv1stcnv  35220  colineardim1  35505  idinside  35528  finminlem  35670  ivthALT  35687  lukshef-ax2  35767  bj-19.41al  36003  bj-equs45fv  36156  bj-elabd2ALT  36272  bj-rest10b  36437  copsex2b  36488  bj-elid6  36518  bj-ccinftydisj  36561  mptsnunlem  36686  topdifinffinlem  36695  relowlssretop  36711  elxp8  36719  fvineqsnf1  36758  pibt1  36764  matunitlindflem1  36951  poimirlem22  36977  poimirlem25  36980  poimirlem27  36982  poimirlem31  36986  ovoliunnfl  36997  itg2addnclem  37006  sstotbnd3  37111  heibor1lem  37144  heibor1  37145  rngmgmbs4  37266  exmid2  37434  redundss3  37965  redundpim3  37967  dalem53  39063  dalem54  39064  linepsubN  39090  pmapsub  39106  elpaddri  39140  pclfinN  39238  pclcmpatN  39239  cdlemg33c0  40040  dihatexv2  40677  eldioph4i  42016  acongtr  42183  pwfi2f1o  42304  aaitgo  42370  tfsconcat0b  42562  frege54cor0a  43080  clsf2  43343  ismnushort  43526  dvsconst  43555  mptssid  44406  xlimxrre  45009  icccncfext  45065  stoweidlem17  45195  elaa2  45412  dmfcoafv  46345  elfzelfzlble  46491  prprelprb  46647  fmtnoprmfac1  46695  fmtnoprmfac2  46697  flsqrt  46723  lighneallem3  46737  proththd  46744  evenprm2  46844  gbogbow  46886  2zrngnmrid  47096  rhmsubcALTVlem3  47123  linccl  47260  lincvalpr  47264  lincdifsn  47270  lincext1  47300  lindslinindsimp1  47303  ldepspr  47319  lincresunit3lem1  47325  logblt1b  47415  dignnld  47454  dig1  47459  dignn0flhalflem1  47466  itcovalsucov  47519  line  47583  rrxline  47585  rrxsphere  47599  itschlc0xyqsol1  47617  itsclc0xyqsolr  47620  lubeldm2  47754  glbeldm2  47755  amgmwlem  48014