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  1949  exdistrf  2445  equs45f  2457  moaneu  2616  dariiALT  2659  festinoALT  2668  barocoALT  2670  r19.27v  3166  rspc2ev  3601  reu3  3698  difrab  4281  opthprneg  4829  copsexgw  5450  copsexg  5451  imainss  6127  trssord  6349  ordnbtwn  6427  fof  6772  fv3  6876  fvelimab  6933  dff2  7071  dffo5  7076  foco2  7081  fnsnbOLD  7140  tpres  7175  f13dfv  7249  dff1o6  7250  oprabidw  7418  oprabid  7419  ssoprab2i  7500  ndmovass  7577  ndmovdistr  7578  elovmpt3rab1  7649  tfi  7829  find  7871  releldm2  8022  bropopvvv  8069  bropfvvvvlem  8070  ressuppssdif  8164  omlimcl  8542  odi  8543  ixpf  8893  dif1en  9124  domtrfil  9156  funsnfsupp  9343  hartogs  9497  card2on  9507  zfreg  9548  epfrs  9684  acni3  10000  dfac2b  10084  cflm  10203  axdc2lem  10401  ac6s  10437  ondomon  10516  axregndlem1  10555  axregnd  10557  eltsk2g  10704  grothpw  10779  grothpwex  10780  grothomex  10782  ltexprlem1  10989  ltexprlem4  10992  recexsrlem  11056  elfzp12  13564  hashf1rn  14317  hashdifpr  14380  hashgt23el  14389  hashge2el2dif  14445  ccatsymb  14547  swrdnd0  14622  swrdpfx  14672  pfxpfx  14673  pfxccatin12  14698  cshwidxmod  14768  repswcshw  14777  cshimadifsn  14795  cshimadifsn0  14796  pfxco  14804  wwlktovfo  14924  relexpsucnnl  14996  cau3lem  15321  rlimres  15524  dvdsnegb  16243  dvds2add  16260  dvds2sub  16261  nn0onn  16350  gcd2n0cl  16479  lcmfun  16615  divgcdcoprmex  16636  cncongr1  16637  isfunc  17826  drsdirfi  18266  sgrpidmnd  18666  smndex1iidm  18828  gaid  19231  symg2bas  19323  qusecsub  19765  c0mgm  20368  rhmisrnghm  20389  c0rhm  20443  rhmsubcrngclem1  20575  srhmsubclem1  20586  abvn0b  20745  lmhmlem  20936  prmirredlem  21382  psgndiflemB  21509  ismhp  22027  matsubgcell  22321  tposmap  22344  mat1dim0  22360  mat1dimid  22361  mat1dimscm  22362  mat1dimmul  22363  dmatmul  22384  dmatcrng  22389  scmatcrng  22408  scmatf1  22418  1marepvsma1  22470  maducoeval2  22527  smadiadetlem3lem0  22552  slesolinv  22567  cramerimplem1  22570  cramerimplem2  22571  1pmatscmul  22589  cpmatacl  22603  cpmatmcllem  22605  cpmatmcl  22606  mat2pmatf1  22616  mat2pmatghm  22617  mat2pmatmul  22618  mat2pmatlin  22622  mat2pmatscmxcl  22627  m2cpmmhm  22632  m2pmfzgsumcl  22635  decpmatmul  22659  pmatcollpw2lem  22664  monmatcollpw  22666  pmatcollpwfi  22669  pmatcollpw3fi1lem2  22674  pmatcollpwscmatlem1  22676  pmatcollpwscmatlem2  22677  pmatcollpwscmat  22678  pm2mpghm  22703  pm2mpmhmlem2  22706  pm2mp  22712  chmatcl  22715  chmatval  22716  chmaidscmat  22735  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulcl  22744  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmidgsumm2pm  22756  cpmidpmatlem2  22758  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cpmadugsumfi  22764  cpmidgsum2  22766  cpmadumatpolylem2  22769  cayhamlem2  22771  chcoeffeqlem  22772  cayleyhamilton0  22776  cayleyhamiltonALT  22778  toponcom  22815  neitr  23067  cnprest  23176  nrmsep2  23243  bwth  23297  2ndcsep  23346  isref  23396  reghaus  23712  isfil2  23743  alexsubALTlem3  23936  cnextcn  23954  lpbl  24391  cmodscmulexp  25022  iscau4  25179  caussi  25197  cmetcusp  25254  ovolicc2lem3  25420  limcresi  25786  elply2  26101  elqaa  26230  aannenlem1  26236  aannenlem2  26237  relogbreexp  26685  cxplogb  26696  bpos1lem  27193  noetalem2  27654  tgjustc1  28402  tgjustc2  28403  axcont  28903  usgrexmplef  29186  subupgr  29214  cplgr3v  29362  cusgrfilem2  29384  usgredgsscusgredg  29387  rusgrprop0  29495  uspgr2wlkeqi  29576  trlontrl  29639  spthonpthon  29681  usgr2wlkspthlem1  29687  usgr2wlkspthlem2  29688  clwlkcompim  29710  clwlkl1loop  29713  wwlksnred  29822  clwwlknonwwlknonb  30035  clwwlknun  30041  1pthon2v  30082  frcond1  30195  frcond4  30199  frgrnbnb  30222  clwlknon2num  30297  numclwlk1lem1  30298  numclwlk1lem2  30299  numclwwlkovh  30302  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwwlk2  30310  isgrpo  30426  vcz  30504  hvsub4  30966  hvaddsub4  31007  5oalem2  31584  5oalem5  31587  5oalem6  31588  3oalem2  31592  homcl  31675  hoadddi  31732  stle0i  32168  spansncv2  32222  mdsymlem1  32332  cdj3lem1  32363  f1ocnt  32725  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  crefdf  33838  sxbrsigalem0  34262  dya2icoseg2  34269  eulerpartlemgvv  34367  ballotlemirc  34523  bnj168  34720  bnj546  34886  bnj594  34902  bnj1097  34971  bnj1110  34972  bnj1174  34993  bnj1176  34995  cusgredgex2  35110  acycgrislfgr  35139  umgracycusgr  35141  cusgracyclt3v  35143  satfv1  35350  satf0suclem  35362  fmlasuc0  35371  fmlafvel  35372  satffunlem2lem1  35391  satfun  35398  fv1stcnv  35764  colineardim1  36049  idinside  36072  finminlem  36306  ivthALT  36323  lukshef-ax2  36403  bj-19.41al  36647  bj-equs45fv  36799  bj-elabd2ALT  36913  bj-rest10b  37077  copsex2b  37128  bj-elid6  37158  bj-ccinftydisj  37201  mptsnunlem  37326  topdifinffinlem  37335  relowlssretop  37351  elxp8  37359  fvineqsnf1  37398  pibt1  37404  matunitlindflem1  37610  poimirlem22  37636  poimirlem25  37639  poimirlem27  37641  poimirlem31  37645  ovoliunnfl  37656  itg2addnclem  37665  sstotbnd3  37770  heibor1lem  37803  heibor1  37804  rngmgmbs4  37925  exmid2  38093  redundss3  38619  redundpim3  38621  dalem53  39719  dalem54  39720  linepsubN  39746  pmapsub  39762  elpaddri  39796  pclfinN  39894  pclcmpatN  39895  cdlemg33c0  40696  dihatexv2  41333  eldioph4i  42800  acongtr  42967  pwfi2f1o  43085  aaitgo  43151  tfsconcat0b  43335  frege54cor0a  43852  clsf2  44115  ismnushort  44290  dvsconst  44319  mptssid  45235  xlimxrre  45829  icccncfext  45885  dvmptfprod  45943  stoweidlem17  46015  elaa2  46232  dmfcoafv  47176  elfzelfzlble  47322  prprelprb  47518  fmtnoprmfac1  47566  fmtnoprmfac2  47568  flsqrt  47594  lighneallem3  47608  proththd  47615  evenprm2  47715  gbogbow  47757  clnbgrel  47829  clnbgredg  47840  uhgrimisgrgric  47931  isubgr3stgrlem1  47965  isubgr3stgr  47974  gpg3nbgrvtx0  48067  gpgvtxdg3  48073  2zrngnmrid  48244  rhmsubcALTVlem3  48271  linccl  48403  lincvalpr  48407  lincdifsn  48413  lincext1  48443  lindslinindsimp1  48446  ldepspr  48462  lincresunit3lem1  48468  logblt1b  48553  dignnld  48592  dig1  48597  dignn0flhalflem1  48604  itcovalsucov  48657  line  48721  rrxline  48723  rrxsphere  48737  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  lubeldm2  48944  glbeldm2  48945  isinito4a  49537  amgmwlem  49791