Theorem anim2i 591

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sylanl2  681  sylanr2  683  andi  907  sbimi  1873  exdistrf  2321  equs45f  2338  moaneu  2521  darii  2553  festino  2559  baroco  2560  r19.27v  3052  rspc2ev  3295  reu3  3363  difrab  3860  copsexg  4882  imainss  5467  trssord  5657  ordnbtwn  5733  ordnbtwnOLD  5734  fof  6028  f1ocnv  6062  fv3  6116  fvelimab  6163  dff2  6279  dffo5  6284  foco2  6287  fnsnb  6337  tpres  6371  f13dfv  6430  dff1o6  6431  oprabid  6576  ssoprab2i  6647  ndmovass  6720  ndmovdistr  6721  elovmpt3rab1  6791  tfi  6945  find  6983  releldm2  7109  bropopvvv  7142  bropfvvvvlem  7143  ressuppssdif  7203  supp0cosupp0  7221  imacosupp  7222  dfrecs3  7356  omlimcl  7545  odi  7546  ixpf  7816  infcntss  8119  funsnfsupp  8182  hartogs  8332  card2on  8342  zfreg  8383  epfrs  8490  acni3  8753  dfac2  8836  cflm  8955  axdc2lem  9153  ac6s  9189  ondomon  9264  axregndlem1  9303  axregnd  9305  eltsk2g  9452  grothpw  9527  grothpwex  9528  grothomex  9530  ltexprlem1  9737  ltexprlem4  9740  recexsrlem  9803  lediv2a  10796  lbreu  10852  elfzp12  12288  dfceil2  12502  focdmex  13001  hashf1rn  13004  hashdifpr  13064  hashge2el2dif  13117  ccatsymb  13219  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12  13342  repswsymball  13377  cshwidxmod  13400  repswcshw  13409  cshimadifsn  13426  cshimadifsn0  13427  wwlktovfo  13549  relexpsucnnl  13620  cau3lem  13942  rlimres  14137  dvdsnegb  14837  dvds2add  14853  dvds2sub  14854  ndvdssub  14971  gcd2n0cl  15069  lcmfun  15196  divgcdcoprmex  15218  cncongr1  15219  powm2modprm  15346  cshwshashlem2  15641  isfunc  16347  drsdirfi  16761  gimcnv  17532  gaid  17555  symg2bas  17641  gsummptnn0fz  18205  lmhmlem  18850  lmimcnv  18888  abvn0b  19123  prmirredlem  19660  psgndiflemB  19765  matbas2  20046  matsubgcell  20059  tposmap  20082  mat1dim0  20098  mat1dimid  20099  mat1dimscm  20100  mat1dimmul  20101  dmatmul  20122  dmatcrng  20127  scmatcrng  20146  scmatf1  20156  1marepvsma1  20208  maducoeval2  20265  smadiadetlem3lem0  20290  slesolinv  20305  cramerimplem1  20308  cramerimplem2  20309  1pmatscmul  20326  cpmatacl  20340  cpmatmcllem  20342  cpmatmcl  20343  mat2pmatf1  20353  mat2pmatghm  20354  mat2pmatmul  20355  mat2pmatlin  20359  mat2pmatscmxcl  20364  m2cpmmhm  20369  m2pmfzgsumcl  20372  m2cpmrngiso  20382  decpmatmul  20396  pmatcollpw2lem  20401  monmatcollpw  20403  pmatcollpwfi  20406  pmatcollpw3fi1lem2  20411  pmatcollpwscmatlem1  20413  pmatcollpwscmatlem2  20414  pmatcollpwscmat  20415  pm2mpghm  20440  pm2mpmhmlem2  20443  pm2mp  20449  chmatcl  20452  chmatval  20453  chmaidscmat  20472  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulcl  20481  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmidgsumm2pm  20493  cpmidpmatlem2  20495  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmidgsum2  20503  cpmadumatpolylem2  20506  cayhamlem2  20508  chcoeffeqlem  20509  cayleyhamilton0  20513  cayleyhamiltonALT  20515  toponcom  20545  neitr  20794  cnprest  20903  nrmsep2  20970  bwth  21023  2ndcsep  21072  isref  21122  reghaus  21438  isfil2  21470  alexsubALTlem3  21663  cnextcn  21681  lpbl  22118  cmodscmulexp  22730  iscau4  22885  caussi  22903  cmetcusp  22958  ovolicc2lem3  23094  limcresi  23455  elply2  23756  elqaa  23881  aannenlem1  23887  aannenlem2  23888  relogbreexp  24313  cxplogb  24324  bpos1lem  24807  lgsqrmodndvds  24878  axcont  25656  structvtxval  25698  structiedg0val  25699  uhgrares  25837  usgraop  25879  usgrares  25898  usgraexmplef  25929  cusgra3v  25993  cusgrafilem2  26008  redwlk  26136  wlkdvspthlem  26137  cyclispthon  26161  usgrcyclnl1  26168  3v3e3cycl1  26172  wwlknimp  26215  wlkiswwlkfun  26245  wlkiswwlkinj  26246  wwlknred  26251  wwlknextbi  26253  wwlknfi  26266  clwwlknprop  26300  wwlkext2clwwlk  26331  clwwnisshclwwn  26337  eleclclwwlknlem1  26345  clwlkfoclwwlk  26372  2wlkonotv  26404  clwlknclwlkdifs  26487  eupatrl  26495  frgraunss  26522  frgranbnb  26547  frgrawopreg  26576  frg2woteq  26587  numclwlk3lem3  26600  numclwwlkffin  26609  numclwwlkovf2ex  26613  numclwwlk1  26625  numclwwlkqhash  26627  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwwlk5  26639  numclwwlk7  26641  frgraregord013  26645  isgrpo  26735  vcz  26814  hvsub4  27278  hvaddsub4  27319  5oalem2  27898  5oalem5  27901  5oalem6  27902  3oalem2  27906  homcl  27989  hoadddi  28046  stle0i  28482  spansncv2  28536  mdsymlem1  28646  cdj3lem1  28677  disjin  28781  disjin2  28782  f1ocnt  28946  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  pmtrprfv2  29179  crefdf  29243  sxbrsigalem0  29660  dya2icoseg2  29667  eulerpartlemgvv  29765  ballotlemirc  29920  bnj145OLD  30049  bnj168  30052  bnj546  30220  bnj594  30236  bnj1097  30303  bnj1110  30304  bnj1174  30325  bnj1176  30327  fv1stcnv  30925  colineardim1  31338  idinside  31361  finminlem  31482  ivthALT  31500  lukshef-ax2  31584  bj-19.41al  31826  bj-equs45fv  31940  bj-rest10b  32223  bj-toprntopon  32244  bj-ccinftydisj  32277  mptsnunlem  32361  topdifinffinlem  32371  relowlssretop  32387  elxp8  32395  matunitlindflem1  32575  poimirlem22  32601  poimirlem25  32604  poimirlem27  32606  poimirlem31  32610  ovoliunnfl  32621  itg2addnclem  32631  indexa  32698  sstotbnd3  32745  heibor1lem  32778  heibor1  32779  rngmgmbs4  32900  exmid2  33071  dalem53  34029  dalem54  34030  linepsubN  34056  pmapsub  34072  elpaddri  34106  pclfinN  34204  pclcmpatN  34205  cdlemg33c0  35008  dihatexv2  35646  eldioph4i  36394  acongtr  36563  pwfi2f1o  36684  aaitgo  36751  frege54cor0a  37177  clsf2  37444  dvsconst  37551  icccncfext  38773  stoweidlem17  38910  elaa2  39127  dmfcoafv  39904  fmtnoprmfac1  40015  fmtnoprmfac2  40017  flsqrt  40046  lighneallem3  40062  proththd  40069  evenprm2  40161  gboagbo  40178  pfxn0  40257  swrdpfx  40277  pfxpfx  40278  pfxccatin12lem2  40287  pfxccatin12  40288  repswpfx  40299  pfxco  40301  elfzelfzlble  40358  subupgr  40511  cplgr3v  40657  cusgrfilem2  40672  usgredgsscusgredg  40675  rusgrprop0  40767  uspgr2wlkeqi  40856  upgrwlkdvde  40943  spthonpthon  40957  usgr2wlkspthlem1  40963  usgr2wlkspthlem2  40964  usgr2trlncl  40966  clWlkcompim  40987  clwlkl1loop  40989  wlkwwlkinj  41093  wwlksnred  41098  wwlksnextbi  41100  wwlksnfi  41112  clwwlknclwwlkdifs  41181  clwlksf1clwwlklem0  41271  clwwlksnun  41281  1pthon2v-av  41320  frcond1  41438  frgrnbnb  41463  frgrwopreg  41486  av-numclwlk3lem3  41506  av-extwwlkfablem2  41510  av-extwwlkfab  41520  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwwlk2  41537  av-frgraregord013  41549  c0mgm  41699  c0rhm  41702  rhmisrnghm  41710  lidlmmgm  41715  2zrngnmrid  41740  rhmsubcrngclem1  41819  srhmsubclem1  41865  srhmsubcALTVlem1  41884  rhmsubcALTVlem3  41899  linccl  41997  lincvalpr  42001  lincdifsn  42007  lincext1  42037  lindslinindsimp1  42040  ldepspr  42056  lincresunit3lem1  42062  logblt1b  42156  dignnld  42195  dig1  42200  dignn0flhalflem1  42207  amgmwlem  42357