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 396

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 206  df-an 397

This theorem is referenced by:  sylanr2  680  andi  1005  19.41v  1954  exdistrf  2448  equs45f  2460  moaneu  2626  dariiALT  2668  festinoALT  2677  barocoALT  2679  r19.27v  3116  rspc2ev  3573  reu3  3663  difrab  4243  opthprneg  4796  copsexgw  5405  copsexg  5406  imainss  6062  trssord  6287  ordnbtwn  6360  fof  6697  fv3  6801  fvelimab  6850  dff2  6984  dffo5  6989  foco2  6992  fnsnb  7047  tpres  7085  f13dfv  7155  dff1o6  7156  oprabidw  7315  oprabid  7316  ssoprab2i  7394  ndmovass  7469  ndmovdistr  7470  elovmpt3rab1  7538  tfi  7709  find  7752  findOLD  7753  releldm2  7893  bropopvvv  7939  bropfvvvvlem  7940  ressuppssdif  8010  omlimcl  8418  odi  8419  ixpf  8717  domtrfil  8987  funsnfsupp  9161  hartogs  9312  card2on  9322  zfreg  9363  epfrs  9498  acni3  9812  dfac2b  9895  cflm  10015  axdc2lem  10213  ac6s  10249  ondomon  10328  axregndlem1  10367  axregnd  10369  eltsk2g  10516  grothpw  10591  grothpwex  10592  grothomex  10594  ltexprlem1  10801  ltexprlem4  10804  recexsrlem  10868  elfzp12  13344  focdmex  14074  hashf1rn  14076  hashdifpr  14139  hashgt23el  14148  hashge2el2dif  14203  ccatsymb  14296  swrdnd0  14379  swrdpfx  14429  pfxpfx  14430  pfxccatin12  14455  cshwidxmod  14525  repswcshw  14534  cshimadifsn  14551  cshimadifsn0  14552  pfxco  14560  wwlktovfo  14682  relexpsucnnl  14750  cau3lem  15075  rlimres  15276  dvdsnegb  15992  dvds2add  16008  dvds2sub  16009  nn0onn  16098  gcd2n0cl  16225  lcmfun  16359  divgcdcoprmex  16380  cncongr1  16381  isfunc  17588  drsdirfi  18032  sgrpidmnd  18399  smndex1iidm  18549  gaid  18914  symg2bas  19009  lmhmlem  20300  abvn0b  20582  prmirredlem  20703  psgndiflemB  20814  matsubgcell  21592  tposmap  21615  mat1dim0  21631  mat1dimid  21632  mat1dimscm  21633  mat1dimmul  21634  dmatmul  21655  dmatcrng  21660  scmatcrng  21679  scmatf1  21689  1marepvsma1  21741  maducoeval2  21798  smadiadetlem3lem0  21823  slesolinv  21838  cramerimplem1  21841  cramerimplem2  21842  1pmatscmul  21860  cpmatacl  21874  cpmatmcllem  21876  cpmatmcl  21877  mat2pmatf1  21887  mat2pmatghm  21888  mat2pmatmul  21889  mat2pmatlin  21893  mat2pmatscmxcl  21898  m2cpmmhm  21903  m2pmfzgsumcl  21906  m2cpmrngiso  21916  decpmatmul  21930  pmatcollpw2lem  21935  monmatcollpw  21937  pmatcollpwfi  21940  pmatcollpw3fi1lem2  21945  pmatcollpwscmatlem1  21947  pmatcollpwscmatlem2  21948  pmatcollpwscmat  21949  pm2mpghm  21974  pm2mpmhmlem2  21977  pm2mp  21983  chmatcl  21986  chmatval  21987  chmaidscmat  22006  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmulcl  22015  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmidgsumm2pm  22027  cpmidpmatlem2  22029  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmidgsum2  22037  cpmadumatpolylem2  22040  cayhamlem2  22042  chcoeffeqlem  22043  cayleyhamilton0  22047  cayleyhamiltonALT  22049  toponcom  22086  neitr  22340  cnprest  22449  nrmsep2  22516  bwth  22570  2ndcsep  22619  isref  22669  reghaus  22985  isfil2  23016  alexsubALTlem3  23209  cnextcn  23227  lpbl  23668  cmodscmulexp  24294  iscau4  24452  caussi  24470  cmetcusp  24527  ovolicc2lem3  24692  limcresi  25058  elply2  25366  elqaa  25491  aannenlem1  25497  aannenlem2  25498  relogbreexp  25934  cxplogb  25945  bpos1lem  26439  tgjustc1  26845  tgjustc2  26846  axcont  27353  usgrexmplef  27635  subupgr  27663  cplgr3v  27811  cusgrfilem2  27832  usgredgsscusgredg  27835  rusgrprop0  27943  uspgr2wlkeqi  28024  trlontrl  28088  spthonpthon  28128  usgr2wlkspthlem1  28134  usgr2wlkspthlem2  28135  clwlkcompim  28157  clwlkl1loop  28160  wwlksnred  28266  clwwlknonwwlknonb  28479  clwwlknun  28485  1pthon2v  28526  frcond1  28639  frcond4  28643  frgrnbnb  28666  clwlknon2num  28741  numclwlk1lem1  28742  numclwlk1lem2  28743  numclwwlkovh  28746  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwwlk2  28754  isgrpo  28868  vcz  28946  hvsub4  29408  hvaddsub4  29449  5oalem2  30026  5oalem5  30029  5oalem6  30030  3oalem2  30034  homcl  30117  hoadddi  30174  stle0i  30610  spansncv2  30664  mdsymlem1  30774  cdj3lem1  30805  f1ocnt  31132  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  crefdf  31807  sxbrsigalem0  32247  dya2icoseg2  32254  eulerpartlemgvv  32352  ballotlemirc  32507  bnj168  32718  bnj546  32885  bnj594  32901  bnj1097  32970  bnj1110  32971  bnj1174  32992  bnj1176  32994  cusgredgex2  33093  acycgrislfgr  33123  umgracycusgr  33125  cusgracyclt3v  33127  satfv1  33334  satf0suclem  33346  fmlasuc0  33355  fmlafvel  33356  satffunlem2lem1  33375  satfun  33382  fv1stcnv  33760  noetalem2  33954  colineardim1  34372  idinside  34395  finminlem  34516  ivthALT  34533  lukshef-ax2  34613  bj-19.41al  34849  bj-equs45fv  35002  bj-elabd2ALT  35122  bj-rest10b  35269  copsex2b  35320  bj-elid6  35350  bj-ccinftydisj  35393  mptsnunlem  35518  topdifinffinlem  35527  relowlssretop  35543  elxp8  35551  fvineqsnf1  35590  pibt1  35596  matunitlindflem1  35782  poimirlem22  35808  poimirlem25  35811  poimirlem27  35813  poimirlem31  35817  ovoliunnfl  35828  itg2addnclem  35837  sstotbnd3  35943  heibor1lem  35976  heibor1  35977  rngmgmbs4  36098  exmid2  36266  redundss3  36748  redundpim3  36750  dalem53  37746  dalem54  37747  linepsubN  37773  pmapsub  37789  elpaddri  37823  pclfinN  37921  pclcmpatN  37922  cdlemg33c0  38723  dihatexv2  39360  eldioph4i  40641  acongtr  40807  pwfi2f1o  40928  aaitgo  40994  frege54cor0a  41478  clsf2  41743  ismnushort  41926  dvsconst  41955  mptssid  42792  xlimxrre  43379  icccncfext  43435  stoweidlem17  43565  elaa2  43782  dmfcoafv  44678  elfzelfzlble  44824  prprelprb  44980  fmtnoprmfac1  45028  fmtnoprmfac2  45030  flsqrt  45056  lighneallem3  45070  proththd  45077  evenprm2  45177  gbogbow  45219  c0mgm  45478  c0rhm  45481  rhmisrnghm  45489  lidlmmgm  45494  2zrngnmrid  45519  rhmsubcrngclem1  45596  srhmsubclem1  45642  rhmsubcALTVlem3  45675  linccl  45766  lincvalpr  45770  lincdifsn  45776  lincext1  45806  lindslinindsimp1  45809  ldepspr  45825  lincresunit3lem1  45831  logblt1b  45921  dignnld  45960  dig1  45965  dignn0flhalflem1  45972  itcovalsucov  46025  line  46089  rrxline  46091  rrxsphere  46105  itschlc0xyqsol1  46123  itsclc0xyqsolr  46126  lubeldm2  46261  glbeldm2  46262  amgmwlem  46517