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  1984  exdistrf  2479  equs45f  2491  moaneu  2651  dariiALT  2693  festinoALT  2702  barocoALT  2704  r19.27v  3195  reu3  3688  difrab  4266  opthprneg  4823  copsexgwOLD  5466  copsexg  5467  imainss  6157  trssord  6400  ordnbtwn  6479  fof  6821  fv3  6929  fvelimab  6983  dff2  7126  dffo5  7131  foco2  7136  tpres  7233  f13dfv  7308  dff1o6  7309  oprabidw  7477  oprabid  7478  ssoprab2i  7557  ndmovass  7636  ndmovdistr  7637  elovmpt3rab1  7708  tfi  7891  find  7934  releldm2  8081  bropopvvv  8129  bropfvvvvlem  8130  ressuppssdif  8233  omlimcl  8617  odi  8618  ixpf  8979  dif1en  9208  domtrfil  9238  funsnfsupp  9414  hartogs  9568  card2on  9578  zfreg  9620  epfrs  9762  hfuni  9954  acni3  10156  dfac2b  10239  cflm  10357  axdc2lem  10556  ac6s  10592  ondomon  10677  axregndlem1  10717  axregnd  10719  eltsk2g  10866  grothpw  10941  grothpwex  10942  grothomex  10944  ltexprlem1  11151  ltexprlem4  11154  recexsrlem  11218  elfzp12  13767  hashf1rn  14526  hashdifpr  14590  hashgt23el  14599  hashge2el2dif  14655  ccatsymb  14758  swrdnd0  14838  swrdpfx  14887  pfxpfx  14888  pfxccatin12  14913  cshwidxmod  14985  repswcshw  14994  cshimadifsn  15011  cshimadifsn0  15012  pfxco  15020  wwlktovfo  15143  relexpsucnnl  15215  cau3lem  15554  rlimres  15757  dvdsnegb  16475  dvds2add  16492  dvds2sub  16493  nn0onn  16582  gcd2n0cl  16711  lcmfun  16852  divgcdcoprmex  16873  cncongr1  16874  isfunc  18071  drsdirfi  18511  chnrev  18833  sgrpidmnd  18960  smndex1iidm  19129  gaid  19546  symg2bas  19640  qusecsub  20082  gsumle  20392  c0mgm  20722  rhmisrnghm  20744  c0rhm  20819  rhmsubcrngclem1  20951  srhmsubclem1  20962  abvn0b  21126  lmhmlem  21337  unichnlidl  21549  prmirredlem  21811  psgndiflemB  21939  ismhp  22494  matsubgcell  22782  tposmap  22805  mat1dim0  22821  mat1dimid  22822  mat1dimscm  22823  mat1dimmul  22824  dmatmul  22845  dmatcrng  22850  scmatcrng  22869  scmatf1  22879  1marepvsma1  22931  maducoeval2  22988  smadiadetlem3lem0  23013  matunitlindflem1  23027  slesolinv  23031  cramerimplem1  23034  cramerimplem2  23035  1pmatscmul  23053  cpmatacl  23067  cpmatmcllem  23069  cpmatmcl  23070  mat2pmatf1  23080  mat2pmatghm  23081  mat2pmatmul  23082  mat2pmatlin  23086  mat2pmatscmxcl  23091  m2cpmmhm  23096  m2pmfzgsumcl  23099  decpmatmul  23123  pmatcollpw2lem  23128  monmatcollpw  23130  pmatcollpwfi  23133  pmatcollpw3fi1lem2  23138  pmatcollpwscmatlem1  23140  pmatcollpwscmatlem2  23141  pmatcollpwscmat  23142  pm2mpghm  23167  pm2mpmhmlem2  23170  pm2mp  23176  chmatcl  23179  chmatval  23180  chmaidscmat  23199  chfacfisf  23205  chfacfisfcpmat  23206  chfacfscmulcl  23208  chfacfscmul0  23209  chfacfscmulgsum  23211  chfacfpmmul0  23213  chfacfpmmulgsum  23215  chfacfpmmulgsum2  23216  cayhamlem1  23217  cpmidgsumm2pm  23220  cpmidpmatlem2  23222  cpmadugsumlemB  23225  cpmadugsumlemC  23226  cpmadugsumlemF  23227  cpmadugsumfi  23228  cpmidgsum2  23230  cpmadumatpolylem2  23233  cayhamlem2  23235  chcoeffeqlem  23236  cayleyhamilton0  23240  cayleyhamiltonALT  23242  toponcom  23279  neitr  23531  cnprest  23640  nrmsep2  23707  bwth  23761  2ndcsep  23811  isref  23861  reghaus  24177  isfil2  24208  alexsubALTlem3  24401  cnextcn  24419  lpbl  24855  cmodscmulexp  25476  iscau4  25633  caussi  25651  cmetcusp  25708  ovolicc2lem3  25873  limcresi  26238  elply2  26547  elqaa  26678  aannenlem1  26688  aannenlem2  26689  relogbreexp  27136  cxplogb  27147  bpos1lem  27642  noetalem2  28132  tgjustc1  28970  tgjustc2  28971  axcont  29587  usgrexmplef  29873  subupgr  29901  cplgr3v  30049  cusgrfilem2  30070  usgredgsscusgredg  30073  rusgrprop0  30181  uspgr2wlkeqi  30261  trlontrl  30326  spthonpthon  30370  usgr2wlkspthlem1  30376  usgr2wlkspthlem2  30377  clwlkcompim  30400  clwlkl1loop  30403  wwlksnred  30514  clwwlknonwwlknonb  30730  clwwlknun  30736  1pthon2v  30787  frcond1  30900  frcond4  30904  frgrnbnb  30927  clwlknon2num  31002  numclwlk1lem1  31003  numclwlk1lem2  31004  numclwwlkovh  31007  numclwwlk2lem1  31010  numclwlk2lem2f  31011  numclwwlk2  31015  isgrpo  31132  vcz  31210  hvsub4  31672  hvaddsub4  31713  5oalem2  32290  5oalem5  32293  5oalem6  32294  3oalem2  32298  homcl  32381  hoadddi  32438  stle0i  32874  spansncv2  32928  mdsymlem1  33038  cdj3lem1  33069  f1ocnt  33465  gsumvsca1  33863  gsumvsca2  33864  crefdf  34563  sxbrsigalem0  34986  dya2icoseg2  34993  eulerpartlemgvv  35091  ballotlemirc  35247  bnj168  35444  bnj546  35609  bnj594  35625  bnj1097  35694  bnj1110  35695  bnj1174  35716  bnj1176  35718  axprALT2  35829  cusgredgex2  36077  acycgrislfgr  36087  umgracycusgr  36089  cusgracyclt3v  36091  satfv1  36308  satf0suclem  36320  fmlasuc0  36329  fmlafvel  36330  satffunlem2lem1  36349  satfun  36356  mirimanofffr  36642  fv1stcnv  36732  colineardim1  37017  idinside  37040  finminlem  37297  ivthALT  37314  lukshef-ax2  37394  regsfromregtco  37517  bj-19.41al  37749  bj-equs45fv  37914  bj-elabd2ALT  38029  bj-rest10b  38214  copsex2b  38266  bj-elid6  38296  bj-ccinftydisj  38339  mptsnunlem  38466  topdifinffinlem  38475  relowlssretop  38491  elxp8  38499  fvineqsnf1  38538  pibt1  38544  poimirlem22  38765  poimirlem25  38768  poimirlem27  38770  poimirlem31  38774  ovoliunnfl  38785  itg2addnclem  38794  sstotbnd3  38913  heibor1lem  38946  heibor1  38947  rngmgmbs4  39068  exmid2  39234  redundss3  39847  redundpim3  39849  dalem53  40985  dalem54  40986  linepsubN  41012  pmapsub  41028  elpaddri  41062  pclfinN  41160  pclcmpatN  41161  cdlemg33c0  41962  dihatexv2  42599  eldioph4i  44023  acongtr  44189  pwfi2f1o  44302  aaitgo  44367  tfsconcat0b  44551  frege54cor0a  45066  clsf2  45329  ismnushort  45488  dvsconst  45517  mptssid  46468  xlimxrre  47056  icccncfext  47112  dvmptfprod  47170  stoweidlem17  47242  elaa2  47459  dmfcoafv  48460  elfzelfzlble  48606  prprelprb  48814  fmtnoprmfac1  48865  fmtnoprmfac2  48867  flsqrt  48893  lighneallem3  48907  proththd  48914  evenprm2  49027  gbogbow  49069  clnbgrel  49141  clnbgredg  49153  uhgrimisgrgric  49244  isubgr3stgrlem1  49279  isubgr3stgr  49288  gpg3nbgrvtx0  49389  gpgvtxdg3  49395  2zrngnmrid  49568  rhmsubcALTVlem3  49595  linccl  49741  lincvalpr  49745  lincdifsn  49751  lincext1  49781  lindslinindsimp1  49784  ldepspr  49800  lincresunit3lem1  49806  logblt1b  49891  dignnld  49930  dig1  49935  dignn0flhalflem1  49942  itcovalsucov  49995  line  50060  rrxline  50062  rrxsphere  50075  itschlc0xyqsol1  50093  itsclc0xyqsolr  50096  lubeldm2  50285  glbeldm2  50286  isinito4a  50901  alseuals  51232  ralseurals  51233  amgmwlem  51299