Theorem anim2i 617

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 613	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 207  df-an 396

This theorem is referenced by:  sylanr2  683  andi  1009  19.41v  1950  exdistrf  2447  equs45f  2459  moaneu  2618  dariiALT  2661  festinoALT  2670  barocoALT  2672  r19.27v  3161  rspc2ev  3590  reu3  3686  difrab  4268  opthprneg  4817  copsexgw  5430  copsexg  5431  imainss  6101  trssord  6323  ordnbtwn  6401  fof  6735  fv3  6840  fvelimab  6894  dff2  7032  dffo5  7037  foco2  7042  fnsnbOLD  7100  tpres  7135  f13dfv  7208  dff1o6  7209  oprabidw  7377  oprabid  7378  ssoprab2i  7457  ndmovass  7534  ndmovdistr  7535  elovmpt3rab1  7606  tfi  7783  find  7825  releldm2  7975  bropopvvv  8020  bropfvvvvlem  8021  ressuppssdif  8115  omlimcl  8493  odi  8494  ixpf  8844  dif1en  9071  domtrfil  9101  funsnfsupp  9276  hartogs  9430  card2on  9440  zfreg  9482  epfrs  9621  acni3  9935  dfac2b  10019  cflm  10138  axdc2lem  10336  ac6s  10372  ondomon  10451  axregndlem1  10490  axregnd  10492  eltsk2g  10639  grothpw  10714  grothpwex  10715  grothomex  10717  ltexprlem1  10924  ltexprlem4  10927  recexsrlem  10991  elfzp12  13500  hashf1rn  14256  hashdifpr  14319  hashgt23el  14328  hashge2el2dif  14384  ccatsymb  14487  swrdnd0  14562  swrdpfx  14611  pfxpfx  14612  pfxccatin12  14637  cshwidxmod  14707  repswcshw  14716  cshimadifsn  14733  cshimadifsn0  14734  pfxco  14742  wwlktovfo  14862  relexpsucnnl  14934  cau3lem  15259  rlimres  15462  dvdsnegb  16181  dvds2add  16198  dvds2sub  16199  nn0onn  16288  gcd2n0cl  16417  lcmfun  16553  divgcdcoprmex  16574  cncongr1  16575  isfunc  17768  drsdirfi  18208  chnrev  18530  sgrpidmnd  18644  smndex1iidm  18806  gaid  19209  symg2bas  19303  qusecsub  19745  gsumle  20055  c0mgm  20375  rhmisrnghm  20396  c0rhm  20447  rhmsubcrngclem1  20579  srhmsubclem1  20590  abvn0b  20749  lmhmlem  20961  prmirredlem  21407  psgndiflemB  21535  ismhp  22053  matsubgcell  22347  tposmap  22370  mat1dim0  22386  mat1dimid  22387  mat1dimscm  22388  mat1dimmul  22389  dmatmul  22410  dmatcrng  22415  scmatcrng  22434  scmatf1  22444  1marepvsma1  22496  maducoeval2  22553  smadiadetlem3lem0  22578  slesolinv  22593  cramerimplem1  22596  cramerimplem2  22597  1pmatscmul  22615  cpmatacl  22629  cpmatmcllem  22631  cpmatmcl  22632  mat2pmatf1  22642  mat2pmatghm  22643  mat2pmatmul  22644  mat2pmatlin  22648  mat2pmatscmxcl  22653  m2cpmmhm  22658  m2pmfzgsumcl  22661  decpmatmul  22685  pmatcollpw2lem  22690  monmatcollpw  22692  pmatcollpwfi  22695  pmatcollpw3fi1lem2  22700  pmatcollpwscmatlem1  22702  pmatcollpwscmatlem2  22703  pmatcollpwscmat  22704  pm2mpghm  22729  pm2mpmhmlem2  22732  pm2mp  22738  chmatcl  22741  chmatval  22742  chmaidscmat  22761  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmulcl  22770  chfacfscmul0  22771  chfacfscmulgsum  22773  chfacfpmmul0  22775  chfacfpmmulgsum  22777  chfacfpmmulgsum2  22778  cayhamlem1  22779  cpmidgsumm2pm  22782  cpmidpmatlem2  22784  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  cpmadugsumfi  22790  cpmidgsum2  22792  cpmadumatpolylem2  22795  cayhamlem2  22797  chcoeffeqlem  22798  cayleyhamilton0  22802  cayleyhamiltonALT  22804  toponcom  22841  neitr  23093  cnprest  23202  nrmsep2  23269  bwth  23323  2ndcsep  23372  isref  23422  reghaus  23738  isfil2  23769  alexsubALTlem3  23962  cnextcn  23980  lpbl  24416  cmodscmulexp  25047  iscau4  25204  caussi  25222  cmetcusp  25279  ovolicc2lem3  25445  limcresi  25811  elply2  26126  elqaa  26255  aannenlem1  26261  aannenlem2  26262  relogbreexp  26710  cxplogb  26721  bpos1lem  27218  noetalem2  27679  tgjustc1  28451  tgjustc2  28452  axcont  28952  usgrexmplef  29235  subupgr  29263  cplgr3v  29411  cusgrfilem2  29433  usgredgsscusgredg  29436  rusgrprop0  29544  uspgr2wlkeqi  29624  trlontrl  29685  spthonpthon  29727  usgr2wlkspthlem1  29733  usgr2wlkspthlem2  29734  clwlkcompim  29756  clwlkl1loop  29759  wwlksnred  29868  clwwlknonwwlknonb  30081  clwwlknun  30087  1pthon2v  30128  frcond1  30241  frcond4  30245  frgrnbnb  30268  clwlknon2num  30343  numclwlk1lem1  30344  numclwlk1lem2  30345  numclwwlkovh  30348  numclwwlk2lem1  30351  numclwlk2lem2f  30352  numclwwlk2  30356  isgrpo  30472  vcz  30550  hvsub4  31012  hvaddsub4  31053  5oalem2  31630  5oalem5  31633  5oalem6  31634  3oalem2  31638  homcl  31721  hoadddi  31778  stle0i  32214  spansncv2  32268  mdsymlem1  32378  cdj3lem1  32409  f1ocnt  32777  gsumvsca1  33190  gsumvsca2  33191  crefdf  33856  sxbrsigalem0  34279  dya2icoseg2  34286  eulerpartlemgvv  34384  ballotlemirc  34540  bnj168  34737  bnj546  34903  bnj594  34919  bnj1097  34988  bnj1110  34989  bnj1174  35010  bnj1176  35012  cusgredgex2  35155  acycgrislfgr  35184  umgracycusgr  35186  cusgracyclt3v  35188  satfv1  35395  satf0suclem  35407  fmlasuc0  35416  fmlafvel  35417  satffunlem2lem1  35436  satfun  35443  fv1stcnv  35809  colineardim1  36094  idinside  36117  finminlem  36351  ivthALT  36368  lukshef-ax2  36448  bj-19.41al  36692  bj-equs45fv  36844  bj-elabd2ALT  36958  bj-rest10b  37122  copsex2b  37173  bj-elid6  37203  bj-ccinftydisj  37246  mptsnunlem  37371  topdifinffinlem  37380  relowlssretop  37396  elxp8  37404  fvineqsnf1  37443  pibt1  37449  matunitlindflem1  37655  poimirlem22  37681  poimirlem25  37684  poimirlem27  37686  poimirlem31  37690  ovoliunnfl  37701  itg2addnclem  37710  sstotbnd3  37815  heibor1lem  37848  heibor1  37849  rngmgmbs4  37970  exmid2  38138  redundss3  38664  redundpim3  38666  dalem53  39763  dalem54  39764  linepsubN  39790  pmapsub  39806  elpaddri  39840  pclfinN  39938  pclcmpatN  39939  cdlemg33c0  40740  dihatexv2  41377  eldioph4i  42844  acongtr  43010  pwfi2f1o  43128  aaitgo  43194  tfsconcat0b  43378  frege54cor0a  43895  clsf2  44158  ismnushort  44333  dvsconst  44362  mptssid  45277  xlimxrre  45868  icccncfext  45924  dvmptfprod  45982  stoweidlem17  46054  elaa2  46271  dmfcoafv  47205  elfzelfzlble  47351  prprelprb  47547  fmtnoprmfac1  47595  fmtnoprmfac2  47597  flsqrt  47623  lighneallem3  47637  proththd  47644  evenprm2  47744  gbogbow  47786  clnbgrel  47858  clnbgredg  47870  uhgrimisgrgric  47961  isubgr3stgrlem1  47996  isubgr3stgr  48005  gpg3nbgrvtx0  48106  gpgvtxdg3  48112  2zrngnmrid  48286  rhmsubcALTVlem3  48313  linccl  48445  lincvalpr  48449  lincdifsn  48455  lincext1  48485  lindslinindsimp1  48488  ldepspr  48504  lincresunit3lem1  48510  logblt1b  48595  dignnld  48634  dig1  48639  dignn0flhalflem1  48646  itcovalsucov  48699  line  48763  rrxline  48765  rrxsphere  48779  itschlc0xyqsol1  48797  itsclc0xyqsolr  48800  lubeldm2  48986  glbeldm2  48987  isinito4a  49579  amgmwlem  49833