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  21209  prmirredlem  21332  psgndiflemB  21463  matsubgcell  22256  tposmap  22279  mat1dim0  22295  mat1dimid  22296  mat1dimscm  22297  mat1dimmul  22298  dmatmul  22319  dmatcrng  22324  scmatcrng  22343  scmatf1  22353  1marepvsma1  22405  maducoeval2  22462  smadiadetlem3lem0  22487  slesolinv  22502  cramerimplem1  22505  cramerimplem2  22506  1pmatscmul  22524  cpmatacl  22538  cpmatmcllem  22540  cpmatmcl  22541  mat2pmatf1  22551  mat2pmatghm  22552  mat2pmatmul  22553  mat2pmatlin  22557  mat2pmatscmxcl  22562  m2cpmmhm  22567  m2pmfzgsumcl  22570  decpmatmul  22594  pmatcollpw2lem  22599  monmatcollpw  22601  pmatcollpwfi  22604  pmatcollpw3fi1lem2  22609  pmatcollpwscmatlem1  22611  pmatcollpwscmatlem2  22612  pmatcollpwscmat  22613  pm2mpghm  22638  pm2mpmhmlem2  22641  pm2mp  22647  chmatcl  22650  chmatval  22651  chmaidscmat  22670  chfacfisf  22676  chfacfisfcpmat  22677  chfacfscmulcl  22679  chfacfscmul0  22680  chfacfscmulgsum  22682  chfacfpmmul0  22684  chfacfpmmulgsum  22686  chfacfpmmulgsum2  22687  cayhamlem1  22688  cpmidgsumm2pm  22691  cpmidpmatlem2  22693  cpmadugsumlemB  22696  cpmadugsumlemC  22697  cpmadugsumlemF  22698  cpmadugsumfi  22699  cpmidgsum2  22701  cpmadumatpolylem2  22704  cayhamlem2  22706  chcoeffeqlem  22707  cayleyhamilton0  22711  cayleyhamiltonALT  22713  toponcom  22750  neitr  23004  cnprest  23113  nrmsep2  23180  bwth  23234  2ndcsep  23283  isref  23333  reghaus  23649  isfil2  23680  alexsubALTlem3  23873  cnextcn  23891  lpbl  24332  cmodscmulexp  24969  iscau4  25127  caussi  25145  cmetcusp  25202  ovolicc2lem3  25368  limcresi  25734  elply2  26048  elqaa  26174  aannenlem1  26180  aannenlem2  26181  relogbreexp  26621  cxplogb  26632  bpos1lem  27128  noetalem2  27588  tgjustc1  28159  tgjustc2  28160  axcont  28667  usgrexmplef  28949  subupgr  28977  cplgr3v  29125  cusgrfilem2  29146  usgredgsscusgredg  29149  rusgrprop0  29257  uspgr2wlkeqi  29338  trlontrl  29401  spthonpthon  29441  usgr2wlkspthlem1  29447  usgr2wlkspthlem2  29448  clwlkcompim  29470  clwlkl1loop  29473  wwlksnred  29579  clwwlknonwwlknonb  29792  clwwlknun  29798  1pthon2v  29839  frcond1  29952  frcond4  29956  frgrnbnb  29979  clwlknon2num  30054  numclwlk1lem1  30055  numclwlk1lem2  30056  numclwwlkovh  30059  numclwwlk2lem1  30062  numclwlk2lem2f  30063  numclwwlk2  30067  isgrpo  30183  vcz  30261  hvsub4  30723  hvaddsub4  30764  5oalem2  31341  5oalem5  31344  5oalem6  31345  3oalem2  31349  homcl  31432  hoadddi  31489  stle0i  31925  spansncv2  31979  mdsymlem1  32089  cdj3lem1  32120  f1ocnt  32446  gsumle  32678  gsumvsca1  32807  gsumvsca2  32808  crefdf  33292  sxbrsigalem0  33734  dya2icoseg2  33741  eulerpartlemgvv  33839  ballotlemirc  33994  bnj168  34205  bnj546  34371  bnj594  34387  bnj1097  34456  bnj1110  34457  bnj1174  34478  bnj1176  34480  cusgredgex2  34577  acycgrislfgr  34607  umgracycusgr  34609  cusgracyclt3v  34611  satfv1  34818  satf0suclem  34830  fmlasuc0  34839  fmlafvel  34840  satffunlem2lem1  34859  satfun  34866  fv1stcnv  35218  colineardim1  35503  idinside  35526  finminlem  35667  ivthALT  35684  lukshef-ax2  35764  bj-19.41al  36000  bj-equs45fv  36153  bj-elabd2ALT  36269  bj-rest10b  36434  copsex2b  36485  bj-elid6  36515  bj-ccinftydisj  36558  mptsnunlem  36683  topdifinffinlem  36692  relowlssretop  36708  elxp8  36716  fvineqsnf1  36755  pibt1  36761  matunitlindflem1  36948  poimirlem22  36974  poimirlem25  36977  poimirlem27  36979  poimirlem31  36983  ovoliunnfl  36994  itg2addnclem  37003  sstotbnd3  37108  heibor1lem  37141  heibor1  37142  rngmgmbs4  37263  exmid2  37431  redundss3  37962  redundpim3  37964  dalem53  39060  dalem54  39061  linepsubN  39087  pmapsub  39103  elpaddri  39137  pclfinN  39235  pclcmpatN  39236  cdlemg33c0  40037  dihatexv2  40674  eldioph4i  42013  acongtr  42180  pwfi2f1o  42301  aaitgo  42367  tfsconcat0b  42559  frege54cor0a  43077  clsf2  43340  ismnushort  43523  dvsconst  43552  mptssid  44403  xlimxrre  45006  icccncfext  45062  stoweidlem17  45192  elaa2  45409  dmfcoafv  46342  elfzelfzlble  46488  prprelprb  46644  fmtnoprmfac1  46692  fmtnoprmfac2  46694  flsqrt  46720  lighneallem3  46734  proththd  46741  evenprm2  46841  gbogbow  46883  2zrngnmrid  47093  rhmsubcALTVlem3  47120  linccl  47257  lincvalpr  47261  lincdifsn  47267  lincext1  47297  lindslinindsimp1  47300  ldepspr  47316  lincresunit3lem1  47322  logblt1b  47412  dignnld  47451  dig1  47456  dignn0flhalflem1  47463  itcovalsucov  47516  line  47580  rrxline  47582  rrxsphere  47596  itschlc0xyqsol1  47614  itsclc0xyqsolr  47617  lubeldm2  47751  glbeldm2  47752  amgmwlem  48011