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  1947  exdistrf  2450  equs45f  2462  moaneu  2621  dariiALT  2664  festinoALT  2673  barocoALT  2675  r19.27v  3186  rspc2ev  3635  reu3  3736  difrab  4324  opthprneg  4870  copsexgw  5501  copsexg  5502  imainss  6176  trssord  6403  ordnbtwn  6479  fof  6821  fv3  6925  fvelimab  6981  dff2  7119  dffo5  7124  foco2  7129  fnsnb  7186  tpres  7221  f13dfv  7294  dff1o6  7295  oprabidw  7462  oprabid  7463  ssoprab2i  7544  ndmovass  7621  ndmovdistr  7622  elovmpt3rab1  7693  tfi  7874  find  7918  releldm2  8067  bropopvvv  8114  bropfvvvvlem  8115  ressuppssdif  8209  omlimcl  8615  odi  8616  ixpf  8959  dif1en  9199  domtrfil  9230  funsnfsupp  9430  hartogs  9582  card2on  9592  zfreg  9633  epfrs  9769  acni3  10085  dfac2b  10169  cflm  10288  axdc2lem  10486  ac6s  10522  ondomon  10601  axregndlem1  10640  axregnd  10642  eltsk2g  10789  grothpw  10864  grothpwex  10865  grothomex  10867  ltexprlem1  11074  ltexprlem4  11077  recexsrlem  11141  elfzp12  13640  hashf1rn  14388  hashdifpr  14451  hashgt23el  14460  hashge2el2dif  14516  ccatsymb  14617  swrdnd0  14692  swrdpfx  14742  pfxpfx  14743  pfxccatin12  14768  cshwidxmod  14838  repswcshw  14847  cshimadifsn  14865  cshimadifsn0  14866  pfxco  14874  wwlktovfo  14994  relexpsucnnl  15066  cau3lem  15390  rlimres  15591  dvdsnegb  16308  dvds2add  16324  dvds2sub  16325  nn0onn  16414  gcd2n0cl  16543  lcmfun  16679  divgcdcoprmex  16700  cncongr1  16701  isfunc  17915  drsdirfi  18363  sgrpidmnd  18765  smndex1iidm  18927  gaid  19330  symg2bas  19425  qusecsub  19868  c0mgm  20476  rhmisrnghm  20497  c0rhm  20551  rhmsubcrngclem1  20683  srhmsubclem1  20694  abvn0b  20854  lmhmlem  21046  prmirredlem  21501  psgndiflemB  21636  ismhp  22162  matsubgcell  22456  tposmap  22479  mat1dim0  22495  mat1dimid  22496  mat1dimscm  22497  mat1dimmul  22498  dmatmul  22519  dmatcrng  22524  scmatcrng  22543  scmatf1  22553  1marepvsma1  22605  maducoeval2  22662  smadiadetlem3lem0  22687  slesolinv  22702  cramerimplem1  22705  cramerimplem2  22706  1pmatscmul  22724  cpmatacl  22738  cpmatmcllem  22740  cpmatmcl  22741  mat2pmatf1  22751  mat2pmatghm  22752  mat2pmatmul  22753  mat2pmatlin  22757  mat2pmatscmxcl  22762  m2cpmmhm  22767  m2pmfzgsumcl  22770  decpmatmul  22794  pmatcollpw2lem  22799  monmatcollpw  22801  pmatcollpwfi  22804  pmatcollpw3fi1lem2  22809  pmatcollpwscmatlem1  22811  pmatcollpwscmatlem2  22812  pmatcollpwscmat  22813  pm2mpghm  22838  pm2mpmhmlem2  22841  pm2mp  22847  chmatcl  22850  chmatval  22851  chmaidscmat  22870  chfacfisf  22876  chfacfisfcpmat  22877  chfacfscmulcl  22879  chfacfscmul0  22880  chfacfscmulgsum  22882  chfacfpmmul0  22884  chfacfpmmulgsum  22886  chfacfpmmulgsum2  22887  cayhamlem1  22888  cpmidgsumm2pm  22891  cpmidpmatlem2  22893  cpmadugsumlemB  22896  cpmadugsumlemC  22897  cpmadugsumlemF  22898  cpmadugsumfi  22899  cpmidgsum2  22901  cpmadumatpolylem2  22904  cayhamlem2  22906  chcoeffeqlem  22907  cayleyhamilton0  22911  cayleyhamiltonALT  22913  toponcom  22950  neitr  23204  cnprest  23313  nrmsep2  23380  bwth  23434  2ndcsep  23483  isref  23533  reghaus  23849  isfil2  23880  alexsubALTlem3  24073  cnextcn  24091  lpbl  24532  cmodscmulexp  25169  iscau4  25327  caussi  25345  cmetcusp  25402  ovolicc2lem3  25568  limcresi  25935  elply2  26250  elqaa  26379  aannenlem1  26385  aannenlem2  26386  relogbreexp  26833  cxplogb  26844  bpos1lem  27341  noetalem2  27802  tgjustc1  28498  tgjustc2  28499  axcont  29006  usgrexmplef  29291  subupgr  29319  cplgr3v  29467  cusgrfilem2  29489  usgredgsscusgredg  29492  rusgrprop0  29600  uspgr2wlkeqi  29681  trlontrl  29744  spthonpthon  29784  usgr2wlkspthlem1  29790  usgr2wlkspthlem2  29791  clwlkcompim  29813  clwlkl1loop  29816  wwlksnred  29922  clwwlknonwwlknonb  30135  clwwlknun  30141  1pthon2v  30182  frcond1  30295  frcond4  30299  frgrnbnb  30322  clwlknon2num  30397  numclwlk1lem1  30398  numclwlk1lem2  30399  numclwwlkovh  30402  numclwwlk2lem1  30405  numclwlk2lem2f  30406  numclwwlk2  30410  isgrpo  30526  vcz  30604  hvsub4  31066  hvaddsub4  31107  5oalem2  31684  5oalem5  31687  5oalem6  31688  3oalem2  31692  homcl  31775  hoadddi  31832  stle0i  32268  spansncv2  32322  mdsymlem1  32432  cdj3lem1  32463  f1ocnt  32810  gsumle  33084  gsumvsca1  33215  gsumvsca2  33216  crefdf  33809  sxbrsigalem0  34253  dya2icoseg2  34260  eulerpartlemgvv  34358  ballotlemirc  34513  bnj168  34723  bnj546  34889  bnj594  34905  bnj1097  34974  bnj1110  34975  bnj1174  34996  bnj1176  34998  cusgredgex2  35107  acycgrislfgr  35137  umgracycusgr  35139  cusgracyclt3v  35141  satfv1  35348  satf0suclem  35360  fmlasuc0  35369  fmlafvel  35370  satffunlem2lem1  35389  satfun  35396  fv1stcnv  35758  colineardim1  36043  idinside  36066  finminlem  36301  ivthALT  36318  lukshef-ax2  36398  bj-19.41al  36642  bj-equs45fv  36794  bj-elabd2ALT  36908  bj-rest10b  37072  copsex2b  37123  bj-elid6  37153  bj-ccinftydisj  37196  mptsnunlem  37321  topdifinffinlem  37330  relowlssretop  37346  elxp8  37354  fvineqsnf1  37393  pibt1  37399  matunitlindflem1  37603  poimirlem22  37629  poimirlem25  37632  poimirlem27  37634  poimirlem31  37638  ovoliunnfl  37649  itg2addnclem  37658  sstotbnd3  37763  heibor1lem  37796  heibor1  37797  rngmgmbs4  37918  exmid2  38086  redundss3  38610  redundpim3  38612  dalem53  39708  dalem54  39709  linepsubN  39735  pmapsub  39751  elpaddri  39785  pclfinN  39883  pclcmpatN  39884  cdlemg33c0  40685  dihatexv2  41322  eldioph4i  42800  acongtr  42967  pwfi2f1o  43085  aaitgo  43151  tfsconcat0b  43336  frege54cor0a  43853  clsf2  44116  ismnushort  44297  dvsconst  44326  mptssid  45185  xlimxrre  45787  icccncfext  45843  dvmptfprod  45901  stoweidlem17  45973  elaa2  46190  dmfcoafv  47125  elfzelfzlble  47271  prprelprb  47442  fmtnoprmfac1  47490  fmtnoprmfac2  47492  flsqrt  47518  lighneallem3  47532  proththd  47539  evenprm2  47639  gbogbow  47681  clnbgrel  47753  clnbgredg  47764  uhgrimisgrgric  47837  isubgr3stgrlem1  47869  isubgr3stgr  47878  gpg3nbgrvtx0  47967  gpgvtxdg3  47973  2zrngnmrid  48100  rhmsubcALTVlem3  48127  linccl  48260  lincvalpr  48264  lincdifsn  48270  lincext1  48300  lindslinindsimp1  48303  ldepspr  48319  lincresunit3lem1  48325  logblt1b  48414  dignnld  48453  dig1  48458  dignn0flhalflem1  48465  itcovalsucov  48518  line  48582  rrxline  48584  rrxsphere  48598  itschlc0xyqsol1  48616  itsclc0xyqsolr  48619  lubeldm2  48753  glbeldm2  48754  amgmwlem  49033