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  2478  equs45f  2490  moaneu  2650  dariiALT  2692  festinoALT  2701  barocoALT  2703  r19.27v  3193  rspc2ev  3592  reu3  3688  difrab  4267  opthprneg  4828  copsexgwOLD  5471  copsexg  5472  imainss  6149  trssord  6378  ordnbtwn  6457  fof  6793  fv3  6900  fvelimab  6954  dff2  7096  dffo5  7101  foco2  7106  fnsnbOLD  7168  tpres  7204  f13dfv  7279  dff1o6  7280  oprabidw  7448  oprabid  7449  ssoprab2i  7528  ndmovass  7606  ndmovdistr  7607  elovmpt3rab1  7678  tfi  7853  find  7896  releldm2  8044  bropopvvv  8091  bropfvvvvlem  8092  ressuppssdif  8187  omlimcl  8569  odi  8570  ixpf  8931  dif1en  9160  domtrfil  9190  funsnfsupp  9366  hartogs  9520  card2on  9530  zfreg  9572  epfrs  9714  acni3  10054  dfac2b  10137  cflm  10255  axdc2lem  10454  ac6s  10490  ondomon  10575  axregndlem1  10615  axregnd  10617  eltsk2g  10764  grothpw  10839  grothpwex  10840  grothomex  10842  ltexprlem1  11049  ltexprlem4  11052  recexsrlem  11116  elfzp12  13662  hashf1rn  14420  hashdifpr  14484  hashgt23el  14493  hashge2el2dif  14549  ccatsymb  14652  swrdnd0  14731  swrdpfx  14780  pfxpfx  14781  pfxccatin12  14806  cshwidxmod  14878  repswcshw  14887  cshimadifsn  14904  cshimadifsn0  14905  pfxco  14913  wwlktovfo  15035  relexpsucnnl  15107  cau3lem  15446  rlimres  15649  dvdsnegb  16369  dvds2add  16386  dvds2sub  16387  nn0onn  16476  gcd2n0cl  16605  lcmfun  16741  divgcdcoprmex  16762  cncongr1  16763  isfunc  17959  drsdirfi  18399  chnrev  18721  sgrpidmnd  18847  smndex1iidm  19016  gaid  19432  symg2bas  19526  qusecsub  19968  gsumle  20278  c0mgm  20606  rhmisrnghm  20628  c0rhm  20702  rhmsubcrngclem1  20834  srhmsubclem1  20845  abvn0b  21008  lmhmlem  21219  unichnlidl  21431  prmirredlem  21691  psgndiflemB  21819  ismhp  22374  matsubgcell  22662  tposmap  22685  mat1dim0  22701  mat1dimid  22702  mat1dimscm  22703  mat1dimmul  22704  dmatmul  22725  dmatcrng  22730  scmatcrng  22749  scmatf1  22759  1marepvsma1  22811  maducoeval2  22868  smadiadetlem3lem0  22893  matunitlindflem1  22907  slesolinv  22911  cramerimplem1  22914  cramerimplem2  22915  1pmatscmul  22933  cpmatacl  22947  cpmatmcllem  22949  cpmatmcl  22950  mat2pmatf1  22960  mat2pmatghm  22961  mat2pmatmul  22962  mat2pmatlin  22966  mat2pmatscmxcl  22971  m2cpmmhm  22976  m2pmfzgsumcl  22979  decpmatmul  23003  pmatcollpw2lem  23008  monmatcollpw  23010  pmatcollpwfi  23013  pmatcollpw3fi1lem2  23018  pmatcollpwscmatlem1  23020  pmatcollpwscmatlem2  23021  pmatcollpwscmat  23022  pm2mpghm  23047  pm2mpmhmlem2  23050  pm2mp  23056  chmatcl  23059  chmatval  23060  chmaidscmat  23079  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulcl  23088  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulgsum  23095  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmidgsumm2pm  23100  cpmidpmatlem2  23102  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  cpmadugsumfi  23108  cpmidgsum2  23110  cpmadumatpolylem2  23113  cayhamlem2  23115  chcoeffeqlem  23116  cayleyhamilton0  23120  cayleyhamiltonALT  23122  toponcom  23159  neitr  23411  cnprest  23520  nrmsep2  23587  bwth  23641  2ndcsep  23691  isref  23741  reghaus  24057  isfil2  24088  alexsubALTlem3  24281  cnextcn  24299  lpbl  24735  cmodscmulexp  25356  iscau4  25513  caussi  25531  cmetcusp  25588  ovolicc2lem3  25753  limcresi  26119  elply2  26428  elqaa  26561  aannenlem1  26571  aannenlem2  26572  relogbreexp  27020  cxplogb  27031  bpos1lem  27526  noetalem2  27986  tgjustc1  28824  tgjustc2  28825  axcont  29441  usgrexmplef  29727  subupgr  29755  cplgr3v  29903  cusgrfilem2  29924  usgredgsscusgredg  29927  rusgrprop0  30035  uspgr2wlkeqi  30115  trlontrl  30180  spthonpthon  30224  usgr2wlkspthlem1  30230  usgr2wlkspthlem2  30231  clwlkcompim  30254  clwlkl1loop  30257  wwlksnred  30368  clwwlknonwwlknonb  30584  clwwlknun  30590  1pthon2v  30641  frcond1  30754  frcond4  30758  frgrnbnb  30781  clwlknon2num  30856  numclwlk1lem1  30857  numclwlk1lem2  30858  numclwwlkovh  30861  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwwlk2  30869  isgrpo  30986  vcz  31064  hvsub4  31526  hvaddsub4  31567  5oalem2  32144  5oalem5  32147  5oalem6  32148  3oalem2  32152  homcl  32235  hoadddi  32292  stle0i  32728  spansncv2  32782  mdsymlem1  32892  cdj3lem1  32923  f1ocnt  33279  gsumvsca1  33674  gsumvsca2  33675  crefdf  34366  sxbrsigalem0  34790  dya2icoseg2  34797  eulerpartlemgvv  34895  ballotlemirc  35051  bnj168  35248  bnj546  35413  bnj594  35429  bnj1097  35498  bnj1110  35499  bnj1174  35520  bnj1176  35522  axprALT2  35625  cusgredgex2  35729  acycgrislfgr  35739  umgracycusgr  35741  cusgracyclt3v  35743  satfv1  35950  satf0suclem  35962  fmlasuc0  35971  fmlafvel  35972  satffunlem2lem1  35991  satfun  35998  fv1stcnv  36364  colineardim1  36649  idinside  36672  finminlem  36945  ivthALT  36962  lukshef-ax2  37042  regsfromregtco  37165  bj-19.41al  37397  bj-equs45fv  37562  bj-elabd2ALT  37677  bj-rest10b  37847  copsex2b  37900  bj-elid6  37930  bj-ccinftydisj  37973  mptsnunlem  38100  topdifinffinlem  38109  relowlssretop  38125  elxp8  38133  fvineqsnf1  38172  pibt1  38178  poimirlem22  38399  poimirlem25  38402  poimirlem27  38404  poimirlem31  38408  ovoliunnfl  38419  itg2addnclem  38428  sstotbnd3  38534  heibor1lem  38567  heibor1  38568  rngmgmbs4  38689  exmid2  38855  redundss3  39468  redundpim3  39470  dalem53  40606  dalem54  40607  linepsubN  40633  pmapsub  40649  elpaddri  40683  pclfinN  40781  pclcmpatN  40782  cdlemg33c0  41583  dihatexv2  42220  eldioph4i  43661  acongtr  43827  pwfi2f1o  43945  aaitgo  44011  tfsconcat0b  44195  frege54cor0a  44711  clsf2  44974  ismnushort  45133  dvsconst  45162  mptssid  46078  xlimxrre  46667  icccncfext  46723  dvmptfprod  46781  stoweidlem17  46853  elaa2  47070  dmfcoafv  48071  elfzelfzlble  48217  prprelprb  48425  fmtnoprmfac1  48476  fmtnoprmfac2  48478  flsqrt  48504  lighneallem3  48518  proththd  48525  evenprm2  48638  gbogbow  48680  clnbgrel  48752  clnbgredg  48764  uhgrimisgrgric  48855  isubgr3stgrlem1  48890  isubgr3stgr  48899  gpg3nbgrvtx0  49000  gpgvtxdg3  49006  2zrngnmrid  49179  rhmsubcALTVlem3  49206  linccl  49352  lincvalpr  49356  lincdifsn  49362  lincext1  49392  lindslinindsimp1  49395  ldepspr  49411  lincresunit3lem1  49417  logblt1b  49502  dignnld  49541  dig1  49546  dignn0flhalflem1  49553  itcovalsucov  49606  line  49670  rrxline  49672  rrxsphere  49686  itschlc0xyqsol1  49704  itsclc0xyqsolr  49707  lubeldm2  49890  glbeldm2  49891  isinito4a  50482  alseuals  50761  ralseurals  50762  amgmwlem  50828