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  3578  reu3  3674  difrab  4259  opthprneg  4809  copsexgw  5438  copsexg  5439  imainss  6112  trssord  6334  ordnbtwn  6412  fof  6746  fv3  6852  fvelimab  6906  dff2  7045  dffo5  7050  foco2  7055  fnsnbOLD  7114  tpres  7149  f13dfv  7222  dff1o6  7223  oprabidw  7391  oprabid  7392  ssoprab2i  7471  ndmovass  7548  ndmovdistr  7549  elovmpt3rab1  7620  tfi  7797  find  7839  releldm2  7989  bropopvvv  8033  bropfvvvvlem  8034  ressuppssdif  8128  omlimcl  8506  odi  8507  ixpf  8861  dif1en  9089  domtrfil  9119  funsnfsupp  9298  hartogs  9452  card2on  9462  zfreg  9504  epfrs  9643  acni3  9960  dfac2b  10044  cflm  10163  axdc2lem  10361  ac6s  10397  ondomon  10476  axregndlem1  10516  axregnd  10518  eltsk2g  10665  grothpw  10740  grothpwex  10741  grothomex  10743  ltexprlem1  10950  ltexprlem4  10953  recexsrlem  11017  elfzp12  13548  hashf1rn  14305  hashdifpr  14368  hashgt23el  14377  hashge2el2dif  14433  ccatsymb  14536  swrdnd0  14611  swrdpfx  14660  pfxpfx  14661  pfxccatin12  14686  cshwidxmod  14756  repswcshw  14765  cshimadifsn  14782  cshimadifsn0  14783  pfxco  14791  wwlktovfo  14911  relexpsucnnl  14983  cau3lem  15308  rlimres  15511  dvdsnegb  16233  dvds2add  16250  dvds2sub  16251  nn0onn  16340  gcd2n0cl  16469  lcmfun  16605  divgcdcoprmex  16626  cncongr1  16627  isfunc  17822  drsdirfi  18262  chnrev  18584  sgrpidmnd  18698  smndex1iidm  18860  gaid  19265  symg2bas  19359  qusecsub  19801  gsumle  20111  c0mgm  20430  rhmisrnghm  20451  c0rhm  20502  rhmsubcrngclem1  20634  srhmsubclem1  20645  abvn0b  20804  lmhmlem  21016  prmirredlem  21462  psgndiflemB  21590  ismhp  22116  matsubgcell  22409  tposmap  22432  mat1dim0  22448  mat1dimid  22449  mat1dimscm  22450  mat1dimmul  22451  dmatmul  22472  dmatcrng  22477  scmatcrng  22496  scmatf1  22506  1marepvsma1  22558  maducoeval2  22615  smadiadetlem3lem0  22640  slesolinv  22655  cramerimplem1  22658  cramerimplem2  22659  1pmatscmul  22677  cpmatacl  22691  cpmatmcllem  22693  cpmatmcl  22694  mat2pmatf1  22704  mat2pmatghm  22705  mat2pmatmul  22706  mat2pmatlin  22710  mat2pmatscmxcl  22715  m2cpmmhm  22720  m2pmfzgsumcl  22723  decpmatmul  22747  pmatcollpw2lem  22752  monmatcollpw  22754  pmatcollpwfi  22757  pmatcollpw3fi1lem2  22762  pmatcollpwscmatlem1  22764  pmatcollpwscmatlem2  22765  pmatcollpwscmat  22766  pm2mpghm  22791  pm2mpmhmlem2  22794  pm2mp  22800  chmatcl  22803  chmatval  22804  chmaidscmat  22823  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmulcl  22832  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmidgsumm2pm  22844  cpmidpmatlem2  22846  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmidgsum2  22854  cpmadumatpolylem2  22857  cayhamlem2  22859  chcoeffeqlem  22860  cayleyhamilton0  22864  cayleyhamiltonALT  22866  toponcom  22903  neitr  23155  cnprest  23264  nrmsep2  23331  bwth  23385  2ndcsep  23434  isref  23484  reghaus  23800  isfil2  23831  alexsubALTlem3  24024  cnextcn  24042  lpbl  24478  cmodscmulexp  25099  iscau4  25256  caussi  25274  cmetcusp  25331  ovolicc2lem3  25496  limcresi  25862  elply2  26171  elqaa  26299  aannenlem1  26305  aannenlem2  26306  relogbreexp  26752  cxplogb  26763  bpos1lem  27259  noetalem2  27720  tgjustc1  28557  tgjustc2  28558  axcont  29059  usgrexmplef  29342  subupgr  29370  cplgr3v  29518  cusgrfilem2  29540  usgredgsscusgredg  29543  rusgrprop0  29651  uspgr2wlkeqi  29731  trlontrl  29792  spthonpthon  29834  usgr2wlkspthlem1  29840  usgr2wlkspthlem2  29841  clwlkcompim  29863  clwlkl1loop  29866  wwlksnred  29975  clwwlknonwwlknonb  30191  clwwlknun  30197  1pthon2v  30238  frcond1  30351  frcond4  30355  frgrnbnb  30378  clwlknon2num  30453  numclwlk1lem1  30454  numclwlk1lem2  30455  numclwwlkovh  30458  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwwlk2  30466  isgrpo  30583  vcz  30661  hvsub4  31123  hvaddsub4  31164  5oalem2  31741  5oalem5  31744  5oalem6  31745  3oalem2  31749  homcl  31832  hoadddi  31889  stle0i  32325  spansncv2  32379  mdsymlem1  32489  cdj3lem1  32520  f1ocnt  32888  gsumvsca1  33302  gsumvsca2  33303  crefdf  34008  sxbrsigalem0  34431  dya2icoseg2  34438  eulerpartlemgvv  34536  ballotlemirc  34692  bnj168  34889  bnj546  35054  bnj594  35070  bnj1097  35139  bnj1110  35140  bnj1174  35161  bnj1176  35163  axprALT2  35269  cusgredgex2  35321  acycgrislfgr  35350  umgracycusgr  35352  cusgracyclt3v  35354  satfv1  35561  satf0suclem  35573  fmlasuc0  35582  fmlafvel  35583  satffunlem2lem1  35602  satfun  35609  fv1stcnv  35975  colineardim1  36259  idinside  36282  finminlem  36516  ivthALT  36533  lukshef-ax2  36613  regsfromregtco  36736  bj-19.41al  36969  bj-equs45fv  37134  bj-elabd2ALT  37248  bj-rest10b  37417  copsex2b  37470  bj-elid6  37500  bj-ccinftydisj  37543  mptsnunlem  37668  topdifinffinlem  37677  relowlssretop  37693  elxp8  37701  fvineqsnf1  37740  pibt1  37746  matunitlindflem1  37951  poimirlem22  37977  poimirlem25  37980  poimirlem27  37982  poimirlem31  37986  ovoliunnfl  37997  itg2addnclem  38006  sstotbnd3  38111  heibor1lem  38144  heibor1  38145  rngmgmbs4  38266  exmid2  38434  redundss3  39047  redundpim3  39049  dalem53  40185  dalem54  40186  linepsubN  40212  pmapsub  40228  elpaddri  40262  pclfinN  40360  pclcmpatN  40361  cdlemg33c0  41162  dihatexv2  41799  eldioph4i  43258  acongtr  43424  pwfi2f1o  43542  aaitgo  43608  tfsconcat0b  43792  frege54cor0a  44308  clsf2  44571  ismnushort  44746  dvsconst  44775  mptssid  45688  xlimxrre  46277  icccncfext  46333  dvmptfprod  46391  stoweidlem17  46463  elaa2  46680  dmfcoafv  47635  elfzelfzlble  47781  prprelprb  47989  fmtnoprmfac1  48040  fmtnoprmfac2  48042  flsqrt  48068  lighneallem3  48082  proththd  48089  evenprm2  48202  gbogbow  48244  clnbgrel  48316  clnbgredg  48328  uhgrimisgrgric  48419  isubgr3stgrlem1  48454  isubgr3stgr  48463  gpg3nbgrvtx0  48564  gpgvtxdg3  48570  2zrngnmrid  48744  rhmsubcALTVlem3  48771  linccl  48902  lincvalpr  48906  lincdifsn  48912  lincext1  48942  lindslinindsimp1  48945  ldepspr  48961  lincresunit3lem1  48967  logblt1b  49052  dignnld  49091  dig1  49096  dignn0flhalflem1  49103  itcovalsucov  49156  line  49220  rrxline  49222  rrxsphere  49236  itschlc0xyqsol1  49254  itsclc0xyqsolr  49257  lubeldm2  49443  glbeldm2  49444  isinito4a  50035  amgmwlem  50289