Theorem anim2i 618

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 614	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  684  andi  1010  19.41v  1951  exdistrf  2452  equs45f  2464  moaneu  2624  dariiALT  2667  festinoALT  2676  barocoALT  2678  r19.27v  3167  rspc2ev  3591  reu3  3687  difrab  4272  opthprneg  4823  copsexgw  5446  copsexg  5447  imainss  6120  trssord  6342  ordnbtwn  6420  fof  6754  fv3  6860  fvelimab  6914  dff2  7053  dffo5  7058  foco2  7063  fnsnbOLD  7122  tpres  7157  f13dfv  7230  dff1o6  7231  oprabidw  7399  oprabid  7400  ssoprab2i  7479  ndmovass  7556  ndmovdistr  7557  elovmpt3rab1  7628  tfi  7805  find  7847  releldm2  7997  bropopvvv  8042  bropfvvvvlem  8043  ressuppssdif  8137  omlimcl  8515  odi  8516  ixpf  8870  dif1en  9098  domtrfil  9128  funsnfsupp  9307  hartogs  9461  card2on  9471  zfreg  9513  epfrs  9652  acni3  9969  dfac2b  10053  cflm  10172  axdc2lem  10370  ac6s  10406  ondomon  10485  axregndlem1  10525  axregnd  10527  eltsk2g  10674  grothpw  10749  grothpwex  10750  grothomex  10752  ltexprlem1  10959  ltexprlem4  10962  recexsrlem  11026  elfzp12  13531  hashf1rn  14287  hashdifpr  14350  hashgt23el  14359  hashge2el2dif  14415  ccatsymb  14518  swrdnd0  14593  swrdpfx  14642  pfxpfx  14643  pfxccatin12  14668  cshwidxmod  14738  repswcshw  14747  cshimadifsn  14764  cshimadifsn0  14765  pfxco  14773  wwlktovfo  14893  relexpsucnnl  14965  cau3lem  15290  rlimres  15493  dvdsnegb  16212  dvds2add  16229  dvds2sub  16230  nn0onn  16319  gcd2n0cl  16448  lcmfun  16584  divgcdcoprmex  16605  cncongr1  16606  isfunc  17800  drsdirfi  18240  chnrev  18562  sgrpidmnd  18676  smndex1iidm  18838  gaid  19240  symg2bas  19334  qusecsub  19776  gsumle  20086  c0mgm  20407  rhmisrnghm  20428  c0rhm  20479  rhmsubcrngclem1  20611  srhmsubclem1  20622  abvn0b  20781  lmhmlem  20993  prmirredlem  21439  psgndiflemB  21567  ismhp  22095  matsubgcell  22390  tposmap  22413  mat1dim0  22429  mat1dimid  22430  mat1dimscm  22431  mat1dimmul  22432  dmatmul  22453  dmatcrng  22458  scmatcrng  22477  scmatf1  22487  1marepvsma1  22539  maducoeval2  22596  smadiadetlem3lem0  22621  slesolinv  22636  cramerimplem1  22639  cramerimplem2  22640  1pmatscmul  22658  cpmatacl  22672  cpmatmcllem  22674  cpmatmcl  22675  mat2pmatf1  22685  mat2pmatghm  22686  mat2pmatmul  22687  mat2pmatlin  22691  mat2pmatscmxcl  22696  m2cpmmhm  22701  m2pmfzgsumcl  22704  decpmatmul  22728  pmatcollpw2lem  22733  monmatcollpw  22735  pmatcollpwfi  22738  pmatcollpw3fi1lem2  22743  pmatcollpwscmatlem1  22745  pmatcollpwscmatlem2  22746  pmatcollpwscmat  22747  pm2mpghm  22772  pm2mpmhmlem2  22775  pm2mp  22781  chmatcl  22784  chmatval  22785  chmaidscmat  22804  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulcl  22813  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmidgsumm2pm  22825  cpmidpmatlem2  22827  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmidgsum2  22835  cpmadumatpolylem2  22838  cayhamlem2  22840  chcoeffeqlem  22841  cayleyhamilton0  22845  cayleyhamiltonALT  22847  toponcom  22884  neitr  23136  cnprest  23245  nrmsep2  23312  bwth  23366  2ndcsep  23415  isref  23465  reghaus  23781  isfil2  23812  alexsubALTlem3  24005  cnextcn  24023  lpbl  24459  cmodscmulexp  25090  iscau4  25247  caussi  25265  cmetcusp  25322  ovolicc2lem3  25488  limcresi  25854  elply2  26169  elqaa  26298  aannenlem1  26304  aannenlem2  26305  relogbreexp  26753  cxplogb  26764  bpos1lem  27261  noetalem2  27722  tgjustc1  28559  tgjustc2  28560  axcont  29061  usgrexmplef  29344  subupgr  29372  cplgr3v  29520  cusgrfilem2  29542  usgredgsscusgredg  29545  rusgrprop0  29653  uspgr2wlkeqi  29733  trlontrl  29794  spthonpthon  29836  usgr2wlkspthlem1  29842  usgr2wlkspthlem2  29843  clwlkcompim  29865  clwlkl1loop  29868  wwlksnred  29977  clwwlknonwwlknonb  30193  clwwlknun  30199  1pthon2v  30240  frcond1  30353  frcond4  30357  frgrnbnb  30380  clwlknon2num  30455  numclwlk1lem1  30456  numclwlk1lem2  30457  numclwwlkovh  30460  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwwlk2  30468  isgrpo  30584  vcz  30662  hvsub4  31124  hvaddsub4  31165  5oalem2  31742  5oalem5  31745  5oalem6  31746  3oalem2  31750  homcl  31833  hoadddi  31890  stle0i  32326  spansncv2  32380  mdsymlem1  32490  cdj3lem1  32521  f1ocnt  32890  gsumvsca1  33319  gsumvsca2  33320  crefdf  34025  sxbrsigalem0  34448  dya2icoseg2  34455  eulerpartlemgvv  34553  ballotlemirc  34709  bnj168  34906  bnj546  35071  bnj594  35087  bnj1097  35156  bnj1110  35157  bnj1174  35178  bnj1176  35180  cusgredgex2  35336  acycgrislfgr  35365  umgracycusgr  35367  cusgracyclt3v  35369  satfv1  35576  satf0suclem  35588  fmlasuc0  35597  fmlafvel  35598  satffunlem2lem1  35617  satfun  35624  fv1stcnv  35990  colineardim1  36274  idinside  36297  finminlem  36531  ivthALT  36548  lukshef-ax2  36628  exeltr  36684  regsfromregtr  36687  bj-19.41al  36898  bj-equs45fv  37053  bj-elabd2ALT  37167  bj-rest10b  37336  copsex2b  37389  bj-elid6  37419  bj-ccinftydisj  37462  mptsnunlem  37587  topdifinffinlem  37596  relowlssretop  37612  elxp8  37620  fvineqsnf1  37659  pibt1  37665  matunitlindflem1  37861  poimirlem22  37887  poimirlem25  37890  poimirlem27  37892  poimirlem31  37896  ovoliunnfl  37907  itg2addnclem  37916  sstotbnd3  38021  heibor1lem  38054  heibor1  38055  rngmgmbs4  38176  exmid2  38344  redundss3  38957  redundpim3  38959  dalem53  40095  dalem54  40096  linepsubN  40122  pmapsub  40138  elpaddri  40172  pclfinN  40270  pclcmpatN  40271  cdlemg33c0  41072  dihatexv2  41709  eldioph4i  43163  acongtr  43329  pwfi2f1o  43447  aaitgo  43513  tfsconcat0b  43697  frege54cor0a  44213  clsf2  44476  ismnushort  44651  dvsconst  44680  mptssid  45593  xlimxrre  46183  icccncfext  46239  dvmptfprod  46297  stoweidlem17  46369  elaa2  46586  dmfcoafv  47529  elfzelfzlble  47675  prprelprb  47871  fmtnoprmfac1  47919  fmtnoprmfac2  47921  flsqrt  47947  lighneallem3  47961  proththd  47968  evenprm2  48068  gbogbow  48110  clnbgrel  48182  clnbgredg  48194  uhgrimisgrgric  48285  isubgr3stgrlem1  48320  isubgr3stgr  48329  gpg3nbgrvtx0  48430  gpgvtxdg3  48436  2zrngnmrid  48610  rhmsubcALTVlem3  48637  linccl  48768  lincvalpr  48772  lincdifsn  48778  lincext1  48808  lindslinindsimp1  48811  ldepspr  48827  lincresunit3lem1  48833  logblt1b  48918  dignnld  48957  dig1  48962  dignn0flhalflem1  48969  itcovalsucov  49022  line  49086  rrxline  49088  rrxsphere  49102  itschlc0xyqsol1  49120  itsclc0xyqsolr  49123  lubeldm2  49309  glbeldm2  49310  isinito4a  49901  amgmwlem  50155