Theorem anim2i 626

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylanr2  693  abab  837  andi  1020  19.41v  1968  exdistrf  2477  equs45f  2489  moaneu  2649  dariiALT  2691  festinoALT  2700  barocoALT  2702  r19.27v  3190  rspc2ev  3594  reu3  3689  difrab  4270  opthprneg  4822  copsexgwOLD  5458  copsexg  5459  imainss  6136  trssord  6359  ordnbtwn  6437  fof  6774  fv3  6881  fvelimab  6935  dff2  7076  dffo5  7081  foco2  7086  fnsnbOLD  7146  tpres  7181  f13dfv  7254  dff1o6  7255  oprabidw  7423  oprabid  7424  ssoprab2i  7503  ndmovass  7580  ndmovdistr  7581  elovmpt3rab1  7652  tfi  7829  find  7872  releldm2  8020  bropopvvv  8064  bropfvvvvlem  8065  ressuppssdif  8160  omlimcl  8542  odi  8543  ixpf  8898  dif1en  9126  domtrfil  9156  funsnfsupp  9335  hartogs  9489  card2on  9499  zfreg  9541  epfrs  9683  acni3  10000  dfac2b  10084  cflm  10203  axdc2lem  10402  ac6s  10438  ondomon  10517  axregndlem1  10557  axregnd  10559  eltsk2g  10706  grothpw  10781  grothpwex  10782  grothomex  10784  ltexprlem1  10991  ltexprlem4  10994  recexsrlem  11058  elfzp12  13605  hashf1rn  14362  hashdifpr  14425  hashgt23el  14434  hashge2el2dif  14490  ccatsymb  14593  swrdnd0  14668  swrdpfx  14717  pfxpfx  14718  pfxccatin12  14743  cshwidxmod  14813  repswcshw  14822  cshimadifsn  14839  cshimadifsn0  14840  pfxco  14848  wwlktovfo  14968  relexpsucnnl  15040  cau3lem  15365  rlimres  15568  dvdsnegb  16290  dvds2add  16307  dvds2sub  16308  nn0onn  16397  gcd2n0cl  16526  lcmfun  16662  divgcdcoprmex  16683  cncongr1  16684  isfunc  17880  drsdirfi  18320  chnrev  18642  sgrpidmnd  18756  smndex1iidm  18918  gaid  19322  symg2bas  19416  qusecsub  19858  gsumle  20168  c0mgm  20487  rhmisrnghm  20508  c0rhm  20563  rhmsubcrngclem1  20695  srhmsubclem1  20706  abvn0b  20865  lmhmlem  21076  prmirredlem  21504  psgndiflemB  21632  ismhp  22185  matsubgcell  22474  tposmap  22497  mat1dim0  22513  mat1dimid  22514  mat1dimscm  22515  mat1dimmul  22516  dmatmul  22537  dmatcrng  22542  scmatcrng  22561  scmatf1  22571  1marepvsma1  22623  maducoeval2  22680  smadiadetlem3lem0  22705  slesolinv  22720  cramerimplem1  22723  cramerimplem2  22724  1pmatscmul  22742  cpmatacl  22756  cpmatmcllem  22758  cpmatmcl  22759  mat2pmatf1  22769  mat2pmatghm  22770  mat2pmatmul  22771  mat2pmatlin  22775  mat2pmatscmxcl  22780  m2cpmmhm  22785  m2pmfzgsumcl  22788  decpmatmul  22812  pmatcollpw2lem  22817  monmatcollpw  22819  pmatcollpwfi  22822  pmatcollpw3fi1lem2  22827  pmatcollpwscmatlem1  22829  pmatcollpwscmatlem2  22830  pmatcollpwscmat  22831  pm2mpghm  22856  pm2mpmhmlem2  22859  pm2mp  22865  chmatcl  22868  chmatval  22869  chmaidscmat  22888  chfacfisf  22894  chfacfisfcpmat  22895  chfacfscmulcl  22897  chfacfscmul0  22898  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulgsum  22904  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmidgsumm2pm  22909  cpmidpmatlem2  22911  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  cpmadugsumfi  22917  cpmidgsum2  22919  cpmadumatpolylem2  22922  cayhamlem2  22924  chcoeffeqlem  22925  cayleyhamilton0  22929  cayleyhamiltonALT  22931  toponcom  22968  neitr  23220  cnprest  23329  nrmsep2  23396  bwth  23450  2ndcsep  23499  isref  23549  reghaus  23865  isfil2  23896  alexsubALTlem3  24089  cnextcn  24107  lpbl  24543  cmodscmulexp  25164  iscau4  25321  caussi  25339  cmetcusp  25396  ovolicc2lem3  25561  limcresi  25927  elply2  26236  elqaa  26363  aannenlem1  26369  aannenlem2  26370  relogbreexp  26817  cxplogb  26828  bpos1lem  27323  noetalem2  27783  tgjustc1  28621  tgjustc2  28622  axcont  29123  usgrexmplef  29406  subupgr  29434  cplgr3v  29582  cusgrfilem2  29603  usgredgsscusgredg  29606  rusgrprop0  29714  uspgr2wlkeqi  29794  trlontrl  29855  spthonpthon  29897  usgr2wlkspthlem1  29903  usgr2wlkspthlem2  29904  clwlkcompim  29926  clwlkl1loop  29929  wwlksnred  30038  clwwlknonwwlknonb  30254  clwwlknun  30260  1pthon2v  30301  frcond1  30414  frcond4  30418  frgrnbnb  30441  clwlknon2num  30516  numclwlk1lem1  30517  numclwlk1lem2  30518  numclwwlkovh  30521  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwwlk2  30529  isgrpo  30646  vcz  30724  hvsub4  31186  hvaddsub4  31227  5oalem2  31804  5oalem5  31807  5oalem6  31808  3oalem2  31812  homcl  31895  hoadddi  31952  stle0i  32388  spansncv2  32442  mdsymlem1  32552  cdj3lem1  32583  f1ocnt  32952  gsumvsca1  33367  gsumvsca2  33368  crefdf  34106  sxbrsigalem0  34529  dya2icoseg2  34536  eulerpartlemgvv  34634  ballotlemirc  34790  bnj168  34990  bnj546  35155  bnj594  35171  bnj1097  35240  bnj1110  35241  bnj1174  35262  bnj1176  35264  axprALT2  35369  cusgredgex2  35437  acycgrislfgr  35466  umgracycusgr  35468  cusgracyclt3v  35470  satfv1  35677  satf0suclem  35689  fmlasuc0  35698  fmlafvel  35699  satffunlem2lem1  35718  satfun  35725  fv1stcnv  36091  colineardim1  36375  idinside  36398  finminlem  36642  ivthALT  36659  lukshef-ax2  36739  regsfromregtco  36862  bj-19.41al  37095  bj-equs45fv  37260  bj-elabd2ALT  37374  bj-rest10b  37543  copsex2b  37596  bj-elid6  37626  bj-ccinftydisj  37669  mptsnunlem  37796  topdifinffinlem  37805  relowlssretop  37821  elxp8  37829  fvineqsnf1  37868  pibt1  37874  matunitlindflem1  38079  poimirlem22  38105  poimirlem25  38108  poimirlem27  38110  poimirlem31  38114  ovoliunnfl  38125  itg2addnclem  38134  sstotbnd3  38239  heibor1lem  38272  heibor1  38273  rngmgmbs4  38394  exmid2  38562  redundss3  39175  redundpim3  39177  dalem53  40313  dalem54  40314  linepsubN  40340  pmapsub  40356  elpaddri  40390  pclfinN  40488  pclcmpatN  40489  cdlemg33c0  41290  dihatexv2  41927  eldioph4i  43353  acongtr  43519  pwfi2f1o  43637  aaitgo  43703  tfsconcat0b  43887  frege54cor0a  44403  clsf2  44666  ismnushort  44841  dvsconst  44870  mptssid  45780  xlimxrre  46369  icccncfext  46425  dvmptfprod  46483  stoweidlem17  46555  elaa2  46772  dmfcoafv  47733  elfzelfzlble  47879  prprelprb  48087  fmtnoprmfac1  48138  fmtnoprmfac2  48140  flsqrt  48166  lighneallem3  48180  proththd  48187  evenprm2  48300  gbogbow  48342  clnbgrel  48414  clnbgredg  48426  uhgrimisgrgric  48517  isubgr3stgrlem1  48552  isubgr3stgr  48561  gpg3nbgrvtx0  48662  gpgvtxdg3  48668  2zrngnmrid  48842  rhmsubcALTVlem3  48869  linccl  49000  lincvalpr  49004  lincdifsn  49010  lincext1  49040  lindslinindsimp1  49043  ldepspr  49059  lincresunit3lem1  49065  logblt1b  49150  dignnld  49189  dig1  49194  dignn0flhalflem1  49201  itcovalsucov  49254  line  49318  rrxline  49320  rrxsphere  49334  itschlc0xyqsol1  49352  itsclc0xyqsolr  49355  lubeldm2  49541  glbeldm2  49542  isinito4a  50133  amgmwlem  50387