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  2477  equs45f  2489  moaneu  2649  dariiALT  2691  festinoALT  2700  barocoALT  2702  r19.27v  3192  rspc2ev  3589  reu3  3685  difrab  4264  opthprneg  4825  copsexgwOLD  5461  copsexg  5462  imainss  6143  trssord  6372  ordnbtwn  6451  fof  6788  fv3  6895  fvelimab  6949  dff2  7091  dffo5  7096  foco2  7101  fnsnbOLD  7163  tpres  7199  f13dfv  7274  dff1o6  7275  oprabidw  7443  oprabid  7444  ssoprab2i  7523  ndmovass  7601  ndmovdistr  7602  elovmpt3rab1  7673  tfi  7853  find  7896  releldm2  8043  bropopvvv  8090  bropfvvvvlem  8091  ressuppssdif  8186  omlimcl  8570  odi  8571  ixpf  8932  dif1en  9161  domtrfil  9191  funsnfsupp  9368  hartogs  9522  card2on  9532  zfreg  9574  epfrs  9716  hfuni  9905  acni3  10107  dfac2b  10190  cflm  10308  axdc2lem  10507  ac6s  10543  ondomon  10628  axregndlem1  10668  axregnd  10670  eltsk2g  10817  grothpw  10892  grothpwex  10893  grothomex  10895  ltexprlem1  11102  ltexprlem4  11105  recexsrlem  11169  elfzp12  13717  hashf1rn  14476  hashdifpr  14540  hashgt23el  14549  hashge2el2dif  14605  ccatsymb  14708  swrdnd0  14787  swrdpfx  14836  pfxpfx  14837  pfxccatin12  14862  cshwidxmod  14934  repswcshw  14943  cshimadifsn  14960  cshimadifsn0  14961  pfxco  14969  wwlktovfo  15091  relexpsucnnl  15163  cau3lem  15502  rlimres  15705  dvdsnegb  16423  dvds2add  16440  dvds2sub  16441  nn0onn  16530  gcd2n0cl  16659  lcmfun  16800  divgcdcoprmex  16821  cncongr1  16822  isfunc  18019  drsdirfi  18459  chnrev  18781  sgrpidmnd  18908  smndex1iidm  19077  gaid  19493  symg2bas  19587  qusecsub  20029  gsumle  20339  c0mgm  20669  rhmisrnghm  20691  c0rhm  20766  rhmsubcrngclem1  20898  srhmsubclem1  20909  abvn0b  21073  lmhmlem  21284  unichnlidl  21496  prmirredlem  21758  psgndiflemB  21886  ismhp  22441  matsubgcell  22729  tposmap  22752  mat1dim0  22768  mat1dimid  22769  mat1dimscm  22770  mat1dimmul  22771  dmatmul  22792  dmatcrng  22797  scmatcrng  22816  scmatf1  22826  1marepvsma1  22878  maducoeval2  22935  smadiadetlem3lem0  22960  matunitlindflem1  22974  slesolinv  22978  cramerimplem1  22981  cramerimplem2  22982  1pmatscmul  23000  cpmatacl  23014  cpmatmcllem  23016  cpmatmcl  23017  mat2pmatf1  23027  mat2pmatghm  23028  mat2pmatmul  23029  mat2pmatlin  23033  mat2pmatscmxcl  23038  m2cpmmhm  23043  m2pmfzgsumcl  23046  decpmatmul  23070  pmatcollpw2lem  23075  monmatcollpw  23077  pmatcollpwfi  23080  pmatcollpw3fi1lem2  23085  pmatcollpwscmatlem1  23087  pmatcollpwscmatlem2  23088  pmatcollpwscmat  23089  pm2mpghm  23114  pm2mpmhmlem2  23117  pm2mp  23123  chmatcl  23126  chmatval  23127  chmaidscmat  23146  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmulcl  23155  chfacfscmul0  23156  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmidgsumm2pm  23167  cpmidpmatlem2  23169  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  cpmadugsumfi  23175  cpmidgsum2  23177  cpmadumatpolylem2  23180  cayhamlem2  23182  chcoeffeqlem  23183  cayleyhamilton0  23187  cayleyhamiltonALT  23189  toponcom  23226  neitr  23478  cnprest  23587  nrmsep2  23654  bwth  23708  2ndcsep  23758  isref  23808  reghaus  24124  isfil2  24155  alexsubALTlem3  24348  cnextcn  24366  lpbl  24802  cmodscmulexp  25423  iscau4  25580  caussi  25598  cmetcusp  25655  ovolicc2lem3  25820  limcresi  26185  elply2  26494  elqaa  26627  aannenlem1  26637  aannenlem2  26638  relogbreexp  27085  cxplogb  27096  bpos1lem  27591  noetalem2  28081  tgjustc1  28919  tgjustc2  28920  axcont  29536  usgrexmplef  29822  subupgr  29850  cplgr3v  29998  cusgrfilem2  30019  usgredgsscusgredg  30022  rusgrprop0  30130  uspgr2wlkeqi  30210  trlontrl  30275  spthonpthon  30319  usgr2wlkspthlem1  30325  usgr2wlkspthlem2  30326  clwlkcompim  30349  clwlkl1loop  30352  wwlksnred  30463  clwwlknonwwlknonb  30679  clwwlknun  30685  1pthon2v  30736  frcond1  30849  frcond4  30853  frgrnbnb  30876  clwlknon2num  30951  numclwlk1lem1  30952  numclwlk1lem2  30953  numclwwlkovh  30956  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwwlk2  30964  isgrpo  31081  vcz  31159  hvsub4  31621  hvaddsub4  31662  5oalem2  32239  5oalem5  32242  5oalem6  32243  3oalem2  32247  homcl  32330  hoadddi  32387  stle0i  32823  spansncv2  32877  mdsymlem1  32987  cdj3lem1  33018  f1ocnt  33374  gsumvsca1  33769  gsumvsca2  33770  crefdf  34462  sxbrsigalem0  34886  dya2icoseg2  34893  eulerpartlemgvv  34991  ballotlemirc  35147  bnj168  35344  bnj546  35509  bnj594  35525  bnj1097  35594  bnj1110  35595  bnj1174  35616  bnj1176  35618  axprALT2  35713  cusgredgex2  35876  acycgrislfgr  35886  umgracycusgr  35888  cusgracyclt3v  35890  satfv1  36097  satf0suclem  36109  fmlasuc0  36118  fmlafvel  36119  satffunlem2lem1  36138  satfun  36145  fv1stcnv  36511  colineardim1  36796  idinside  36819  finminlem  37076  ivthALT  37093  lukshef-ax2  37173  regsfromregtco  37296  bj-19.41al  37528  bj-equs45fv  37693  bj-elabd2ALT  37808  bj-rest10b  37978  copsex2b  38029  bj-elid6  38059  bj-ccinftydisj  38102  mptsnunlem  38229  topdifinffinlem  38238  relowlssretop  38254  elxp8  38262  fvineqsnf1  38301  pibt1  38307  poimirlem22  38528  poimirlem25  38531  poimirlem27  38533  poimirlem31  38537  ovoliunnfl  38548  itg2addnclem  38557  sstotbnd3  38678  heibor1lem  38711  heibor1  38712  rngmgmbs4  38833  exmid2  38999  redundss3  39612  redundpim3  39614  dalem53  40750  dalem54  40751  linepsubN  40777  pmapsub  40793  elpaddri  40827  pclfinN  40925  pclcmpatN  40926  cdlemg33c0  41727  dihatexv2  42364  eldioph4i  43772  acongtr  43938  pwfi2f1o  44056  aaitgo  44122  tfsconcat0b  44306  frege54cor0a  44822  clsf2  45085  ismnushort  45244  dvsconst  45273  mptssid  46196  xlimxrre  46785  icccncfext  46841  dvmptfprod  46899  stoweidlem17  46971  elaa2  47188  dmfcoafv  48189  elfzelfzlble  48335  prprelprb  48543  fmtnoprmfac1  48594  fmtnoprmfac2  48596  flsqrt  48622  lighneallem3  48636  proththd  48643  evenprm2  48756  gbogbow  48798  clnbgrel  48870  clnbgredg  48882  uhgrimisgrgric  48973  isubgr3stgrlem1  49008  isubgr3stgr  49017  gpg3nbgrvtx0  49118  gpgvtxdg3  49124  2zrngnmrid  49297  rhmsubcALTVlem3  49324  linccl  49470  lincvalpr  49474  lincdifsn  49480  lincext1  49510  lindslinindsimp1  49513  ldepspr  49529  lincresunit3lem1  49535  logblt1b  49620  dignnld  49659  dig1  49664  dignn0flhalflem1  49671  itcovalsucov  49724  line  49788  rrxline  49790  rrxsphere  49804  itschlc0xyqsol1  49822  itsclc0xyqsolr  49825  lubeldm2  50008  glbeldm2  50009  isinito4a  50600  alseuals  50864  ralseurals  50865  amgmwlem  50931