Theorem anim2i 628

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 624	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylanr2  695  abab  839  andi  1025  19.41v  1979  exdistrf  2479  equs45f  2491  moaneu  2651  dariiALT  2693  festinoALT  2702  barocoALT  2704  r19.27v  3194  rspc2ev  3595  reu3  3691  difrab  4272  opthprneg  4831  copsexgwOLD  5475  copsexg  5476  imainss  6153  trssord  6379  ordnbtwn  6458  fof  6794  fv3  6901  fvelimab  6955  dff2  7096  dffo5  7101  foco2  7106  fnsnbOLD  7166  tpres  7201  f13dfv  7274  dff1o6  7275  oprabidw  7443  oprabid  7444  ssoprab2i  7523  ndmovass  7600  ndmovdistr  7601  elovmpt3rab1  7672  tfi  7850  find  7893  releldm2  8041  bropopvvv  8086  bropfvvvvlem  8087  ressuppssdif  8182  omlimcl  8564  odi  8565  ixpf  8919  dif1en  9147  domtrfil  9177  funsnfsupp  9353  hartogs  9507  card2on  9517  zfreg  9559  epfrs  9701  acni3  10032  dfac2b  10115  cflm  10234  axdc2lem  10433  ac6s  10469  ondomon  10548  axregndlem1  10588  axregnd  10590  eltsk2g  10737  grothpw  10812  grothpwex  10813  grothomex  10815  ltexprlem1  11022  ltexprlem4  11025  recexsrlem  11089  elfzp12  13633  hashf1rn  14390  hashdifpr  14454  hashgt23el  14463  hashge2el2dif  14519  ccatsymb  14622  swrdnd0  14697  swrdpfx  14746  pfxpfx  14747  pfxccatin12  14772  cshwidxmod  14842  repswcshw  14851  cshimadifsn  14868  cshimadifsn0  14869  pfxco  14877  wwlktovfo  14997  relexpsucnnl  15069  cau3lem  15408  rlimres  15611  dvdsnegb  16332  dvds2add  16349  dvds2sub  16350  nn0onn  16439  gcd2n0cl  16568  lcmfun  16704  divgcdcoprmex  16725  cncongr1  16726  isfunc  17922  drsdirfi  18362  chnrev  18684  sgrpidmnd  18798  smndex1iidm  18961  gaid  19370  symg2bas  19464  qusecsub  19906  gsumle  20216  c0mgm  20542  rhmisrnghm  20563  c0rhm  20620  rhmsubcrngclem1  20752  srhmsubclem1  20763  abvn0b  20920  lmhmlem  21131  unichnlidl  21343  prmirredlem  21603  psgndiflemB  21731  ismhp  22284  matsubgcell  22572  tposmap  22595  mat1dim0  22611  mat1dimid  22612  mat1dimscm  22613  mat1dimmul  22614  dmatmul  22635  dmatcrng  22640  scmatcrng  22659  scmatf1  22669  1marepvsma1  22721  maducoeval2  22778  smadiadetlem3lem0  22803  slesolinv  22818  cramerimplem1  22821  cramerimplem2  22822  1pmatscmul  22840  cpmatacl  22854  cpmatmcllem  22856  cpmatmcl  22857  mat2pmatf1  22867  mat2pmatghm  22868  mat2pmatmul  22869  mat2pmatlin  22873  mat2pmatscmxcl  22878  m2cpmmhm  22883  m2pmfzgsumcl  22886  decpmatmul  22910  pmatcollpw2lem  22915  monmatcollpw  22917  pmatcollpwfi  22920  pmatcollpw3fi1lem2  22925  pmatcollpwscmatlem1  22927  pmatcollpwscmatlem2  22928  pmatcollpwscmat  22929  pm2mpghm  22954  pm2mpmhmlem2  22957  pm2mp  22963  chmatcl  22966  chmatval  22967  chmaidscmat  22986  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulcl  22995  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmidgsumm2pm  23007  cpmidpmatlem2  23009  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cpmadugsumfi  23015  cpmidgsum2  23017  cpmadumatpolylem2  23020  cayhamlem2  23022  chcoeffeqlem  23023  cayleyhamilton0  23027  cayleyhamiltonALT  23029  toponcom  23066  neitr  23318  cnprest  23427  nrmsep2  23494  bwth  23548  2ndcsep  23597  isref  23647  reghaus  23963  isfil2  23994  alexsubALTlem3  24187  cnextcn  24205  lpbl  24641  cmodscmulexp  25262  iscau4  25419  caussi  25437  cmetcusp  25494  ovolicc2lem3  25659  limcresi  26025  elply2  26334  elqaa  26464  aannenlem1  26472  aannenlem2  26473  relogbreexp  26921  cxplogb  26932  bpos1lem  27427  noetalem2  27887  tgjustc1  28725  tgjustc2  28726  axcont  29307  usgrexmplef  29590  subupgr  29618  cplgr3v  29766  cusgrfilem2  29787  usgredgsscusgredg  29790  rusgrprop0  29898  uspgr2wlkeqi  29978  trlontrl  30039  spthonpthon  30081  usgr2wlkspthlem1  30087  usgr2wlkspthlem2  30088  clwlkcompim  30110  clwlkl1loop  30113  wwlksnred  30222  clwwlknonwwlknonb  30438  clwwlknun  30444  1pthon2v  30485  frcond1  30598  frcond4  30602  frgrnbnb  30625  clwlknon2num  30700  numclwlk1lem1  30701  numclwlk1lem2  30702  numclwwlkovh  30705  numclwwlk2lem1  30708  numclwlk2lem2f  30709  numclwwlk2  30713  isgrpo  30830  vcz  30908  hvsub4  31370  hvaddsub4  31411  5oalem2  31988  5oalem5  31991  5oalem6  31992  3oalem2  31996  homcl  32079  hoadddi  32136  stle0i  32572  spansncv2  32626  mdsymlem1  32736  cdj3lem1  32767  f1ocnt  33126  gsumvsca1  33527  gsumvsca2  33528  crefdf  34219  sxbrsigalem0  34642  dya2icoseg2  34649  eulerpartlemgvv  34747  ballotlemirc  34903  bnj168  35100  bnj546  35265  bnj594  35281  bnj1097  35350  bnj1110  35351  bnj1174  35372  bnj1176  35374  axprALT2  35484  cusgredgex2  35596  acycgrislfgr  35625  umgracycusgr  35627  cusgracyclt3v  35629  satfv1  35836  satf0suclem  35848  fmlasuc0  35857  fmlafvel  35858  satffunlem2lem1  35877  satfun  35884  fv1stcnv  36250  colineardim1  36534  idinside  36557  finminlem  36810  ivthALT  36827  lukshef-ax2  36907  regsfromregtco  37030  bj-19.41al  37262  bj-equs45fv  37427  bj-elabd2ALT  37542  bj-rest10b  37712  copsex2b  37765  bj-elid6  37795  bj-ccinftydisj  37838  mptsnunlem  37965  topdifinffinlem  37974  relowlssretop  37990  elxp8  37998  fvineqsnf1  38037  pibt1  38043  matunitlindflem1  38248  poimirlem22  38274  poimirlem25  38277  poimirlem27  38279  poimirlem31  38283  ovoliunnfl  38294  itg2addnclem  38303  sstotbnd3  38408  heibor1lem  38441  heibor1  38442  rngmgmbs4  38563  exmid2  38729  redundss3  39342  redundpim3  39344  dalem53  40480  dalem54  40481  linepsubN  40507  pmapsub  40523  elpaddri  40557  pclfinN  40655  pclcmpatN  40656  cdlemg33c0  41457  dihatexv2  42094  eldioph4i  43522  acongtr  43688  pwfi2f1o  43806  aaitgo  43872  tfsconcat0b  44056  frege54cor0a  44572  clsf2  44835  ismnushort  44994  dvsconst  45023  mptssid  45939  xlimxrre  46528  icccncfext  46584  dvmptfprod  46642  stoweidlem17  46714  elaa2  46931  dmfcoafv  47895  elfzelfzlble  48041  prprelprb  48249  fmtnoprmfac1  48300  fmtnoprmfac2  48302  flsqrt  48328  lighneallem3  48342  proththd  48349  evenprm2  48462  gbogbow  48504  clnbgrel  48576  clnbgredg  48588  uhgrimisgrgric  48679  isubgr3stgrlem1  48714  isubgr3stgr  48723  gpg3nbgrvtx0  48824  gpgvtxdg3  48830  2zrngnmrid  49004  rhmsubcALTVlem3  49031  linccl  49177  lincvalpr  49181  lincdifsn  49187  lincext1  49217  lindslinindsimp1  49220  ldepspr  49236  lincresunit3lem1  49242  logblt1b  49327  dignnld  49366  dig1  49371  dignn0flhalflem1  49378  itcovalsucov  49431  line  49495  rrxline  49497  rrxsphere  49511  itschlc0xyqsol1  49529  itsclc0xyqsolr  49532  lubeldm2  49717  glbeldm2  49718  isinito4a  50309  amgmwlem  50585