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  1948  exdistrf  2450  equs45f  2462  moaneu  2621  dariiALT  2664  festinoALT  2673  barocoALT  2675  r19.27v  3175  rspc2ev  3619  reu3  3717  difrab  4300  opthprneg  4847  copsexgw  5477  copsexg  5478  imainss  6156  trssord  6382  ordnbtwn  6458  fof  6801  fv3  6905  fvelimab  6962  dff2  7100  dffo5  7105  foco2  7110  fnsnbOLD  7169  tpres  7204  f13dfv  7277  dff1o6  7278  oprabidw  7445  oprabid  7446  ssoprab2i  7527  ndmovass  7604  ndmovdistr  7605  elovmpt3rab1  7676  tfi  7857  find  7900  releldm2  8051  bropopvvv  8098  bropfvvvvlem  8099  ressuppssdif  8193  omlimcl  8599  odi  8600  ixpf  8943  dif1en  9183  domtrfil  9215  funsnfsupp  9415  hartogs  9567  card2on  9577  zfreg  9618  epfrs  9754  acni3  10070  dfac2b  10154  cflm  10273  axdc2lem  10471  ac6s  10507  ondomon  10586  axregndlem1  10625  axregnd  10627  eltsk2g  10774  grothpw  10849  grothpwex  10850  grothomex  10852  ltexprlem1  11059  ltexprlem4  11062  recexsrlem  11126  elfzp12  13626  hashf1rn  14374  hashdifpr  14437  hashgt23el  14446  hashge2el2dif  14502  ccatsymb  14603  swrdnd0  14678  swrdpfx  14728  pfxpfx  14729  pfxccatin12  14754  cshwidxmod  14824  repswcshw  14833  cshimadifsn  14851  cshimadifsn0  14852  pfxco  14860  wwlktovfo  14980  relexpsucnnl  15052  cau3lem  15376  rlimres  15577  dvdsnegb  16294  dvds2add  16310  dvds2sub  16311  nn0onn  16400  gcd2n0cl  16529  lcmfun  16665  divgcdcoprmex  16686  cncongr1  16687  isfunc  17885  drsdirfi  18326  sgrpidmnd  18726  smndex1iidm  18888  gaid  19291  symg2bas  19383  qusecsub  19826  c0mgm  20432  rhmisrnghm  20453  c0rhm  20507  rhmsubcrngclem1  20639  srhmsubclem1  20650  abvn0b  20810  lmhmlem  21001  prmirredlem  21450  psgndiflemB  21585  ismhp  22111  matsubgcell  22407  tposmap  22430  mat1dim0  22446  mat1dimid  22447  mat1dimscm  22448  mat1dimmul  22449  dmatmul  22470  dmatcrng  22475  scmatcrng  22494  scmatf1  22504  1marepvsma1  22556  maducoeval2  22613  smadiadetlem3lem0  22638  slesolinv  22653  cramerimplem1  22656  cramerimplem2  22657  1pmatscmul  22675  cpmatacl  22689  cpmatmcllem  22691  cpmatmcl  22692  mat2pmatf1  22702  mat2pmatghm  22703  mat2pmatmul  22704  mat2pmatlin  22708  mat2pmatscmxcl  22713  m2cpmmhm  22718  m2pmfzgsumcl  22721  decpmatmul  22745  pmatcollpw2lem  22750  monmatcollpw  22752  pmatcollpwfi  22755  pmatcollpw3fi1lem2  22760  pmatcollpwscmatlem1  22762  pmatcollpwscmatlem2  22763  pmatcollpwscmat  22764  pm2mpghm  22789  pm2mpmhmlem2  22792  pm2mp  22798  chmatcl  22801  chmatval  22802  chmaidscmat  22821  chfacfisf  22827  chfacfisfcpmat  22828  chfacfscmulcl  22830  chfacfscmul0  22831  chfacfscmulgsum  22833  chfacfpmmul0  22835  chfacfpmmulgsum  22837  chfacfpmmulgsum2  22838  cayhamlem1  22839  cpmidgsumm2pm  22842  cpmidpmatlem2  22844  cpmadugsumlemB  22847  cpmadugsumlemC  22848  cpmadugsumlemF  22849  cpmadugsumfi  22850  cpmidgsum2  22852  cpmadumatpolylem2  22855  cayhamlem2  22857  chcoeffeqlem  22858  cayleyhamilton0  22862  cayleyhamiltonALT  22864  toponcom  22901  neitr  23153  cnprest  23262  nrmsep2  23329  bwth  23383  2ndcsep  23432  isref  23482  reghaus  23798  isfil2  23829  alexsubALTlem3  24022  cnextcn  24040  lpbl  24479  cmodscmulexp  25110  iscau4  25268  caussi  25286  cmetcusp  25343  ovolicc2lem3  25509  limcresi  25875  elply2  26190  elqaa  26319  aannenlem1  26325  aannenlem2  26326  relogbreexp  26773  cxplogb  26784  bpos1lem  27281  noetalem2  27742  tgjustc1  28438  tgjustc2  28439  axcont  28940  usgrexmplef  29223  subupgr  29251  cplgr3v  29399  cusgrfilem2  29421  usgredgsscusgredg  29424  rusgrprop0  29532  uspgr2wlkeqi  29613  trlontrl  29676  spthonpthon  29718  usgr2wlkspthlem1  29724  usgr2wlkspthlem2  29725  clwlkcompim  29747  clwlkl1loop  29750  wwlksnred  29859  clwwlknonwwlknonb  30072  clwwlknun  30078  1pthon2v  30119  frcond1  30232  frcond4  30236  frgrnbnb  30259  clwlknon2num  30334  numclwlk1lem1  30335  numclwlk1lem2  30336  numclwwlkovh  30339  numclwwlk2lem1  30342  numclwlk2lem2f  30343  numclwwlk2  30347  isgrpo  30463  vcz  30541  hvsub4  31003  hvaddsub4  31044  5oalem2  31621  5oalem5  31624  5oalem6  31625  3oalem2  31629  homcl  31712  hoadddi  31769  stle0i  32205  spansncv2  32259  mdsymlem1  32369  cdj3lem1  32400  f1ocnt  32751  gsumle  33047  gsumvsca1  33178  gsumvsca2  33179  crefdf  33788  sxbrsigalem0  34214  dya2icoseg2  34221  eulerpartlemgvv  34319  ballotlemirc  34475  bnj168  34685  bnj546  34851  bnj594  34867  bnj1097  34936  bnj1110  34937  bnj1174  34958  bnj1176  34960  cusgredgex2  35069  acycgrislfgr  35098  umgracycusgr  35100  cusgracyclt3v  35102  satfv1  35309  satf0suclem  35321  fmlasuc0  35330  fmlafvel  35331  satffunlem2lem1  35350  satfun  35357  fv1stcnv  35718  colineardim1  36003  idinside  36026  finminlem  36260  ivthALT  36277  lukshef-ax2  36357  bj-19.41al  36601  bj-equs45fv  36753  bj-elabd2ALT  36867  bj-rest10b  37031  copsex2b  37082  bj-elid6  37112  bj-ccinftydisj  37155  mptsnunlem  37280  topdifinffinlem  37289  relowlssretop  37305  elxp8  37313  fvineqsnf1  37352  pibt1  37358  matunitlindflem1  37564  poimirlem22  37590  poimirlem25  37593  poimirlem27  37595  poimirlem31  37599  ovoliunnfl  37610  itg2addnclem  37619  sstotbnd3  37724  heibor1lem  37757  heibor1  37758  rngmgmbs4  37879  exmid2  38047  redundss3  38570  redundpim3  38572  dalem53  39668  dalem54  39669  linepsubN  39695  pmapsub  39711  elpaddri  39745  pclfinN  39843  pclcmpatN  39844  cdlemg33c0  40645  dihatexv2  41282  eldioph4i  42768  acongtr  42935  pwfi2f1o  43053  aaitgo  43119  tfsconcat0b  43304  frege54cor0a  43821  clsf2  44084  ismnushort  44265  dvsconst  44294  mptssid  45192  xlimxrre  45791  icccncfext  45847  dvmptfprod  45905  stoweidlem17  45977  elaa2  46194  dmfcoafv  47133  elfzelfzlble  47279  prprelprb  47450  fmtnoprmfac1  47498  fmtnoprmfac2  47500  flsqrt  47526  lighneallem3  47540  proththd  47547  evenprm2  47647  gbogbow  47689  clnbgrel  47761  clnbgredg  47772  uhgrimisgrgric  47845  isubgr3stgrlem1  47879  isubgr3stgr  47888  gpg3nbgrvtx0  47978  gpgvtxdg3  47984  2zrngnmrid  48118  rhmsubcALTVlem3  48145  linccl  48277  lincvalpr  48281  lincdifsn  48287  lincext1  48317  lindslinindsimp1  48320  ldepspr  48336  lincresunit3lem1  48342  logblt1b  48431  dignnld  48470  dig1  48475  dignn0flhalflem1  48482  itcovalsucov  48535  line  48599  rrxline  48601  rrxsphere  48615  itschlc0xyqsol1  48633  itsclc0xyqsolr  48636  lubeldm2  48801  glbeldm2  48802  amgmwlem  49317