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 397

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 398

This theorem is referenced by:  sylanr2  682  andi  1007  19.41v  1954  exdistrf  2447  equs45f  2459  moaneu  2620  dariiALT  2662  festinoALT  2671  barocoALT  2673  r19.27v  3188  rspc2ev  3624  reu3  3723  difrab  4308  opthprneg  4865  copsexgw  5490  copsexg  5491  imainss  6151  trssord  6379  ordnbtwn  6455  fof  6803  fv3  6907  fvelimab  6962  dff2  7098  dffo5  7103  foco2  7106  fnsnb  7161  tpres  7199  f13dfv  7269  dff1o6  7270  oprabidw  7437  oprabid  7438  ssoprab2i  7516  ndmovass  7592  ndmovdistr  7593  elovmpt3rab1  7663  tfi  7839  find  7884  findOLD  7885  releldm2  8026  bropopvvv  8073  bropfvvvvlem  8074  ressuppssdif  8167  omlimcl  8575  odi  8576  ixpf  8911  dif1en  9157  domtrfil  9192  funsnfsupp  9384  hartogs  9536  card2on  9546  zfreg  9587  epfrs  9723  acni3  10039  dfac2b  10122  cflm  10242  axdc2lem  10440  ac6s  10476  ondomon  10555  axregndlem1  10594  axregnd  10596  eltsk2g  10743  grothpw  10818  grothpwex  10819  grothomex  10821  ltexprlem1  11028  ltexprlem4  11031  recexsrlem  11095  elfzp12  13577  hashf1rn  14309  hashdifpr  14372  hashgt23el  14381  hashge2el2dif  14438  ccatsymb  14529  swrdnd0  14604  swrdpfx  14654  pfxpfx  14655  pfxccatin12  14680  cshwidxmod  14750  repswcshw  14759  cshimadifsn  14777  cshimadifsn0  14778  pfxco  14786  wwlktovfo  14906  relexpsucnnl  14974  cau3lem  15298  rlimres  15499  dvdsnegb  16214  dvds2add  16230  dvds2sub  16231  nn0onn  16320  gcd2n0cl  16447  lcmfun  16579  divgcdcoprmex  16600  cncongr1  16601  isfunc  17811  drsdirfi  18255  sgrpidmnd  18627  smndex1iidm  18779  gaid  19158  symg2bas  19255  qusecsub  19698  lmhmlem  20633  abvn0b  20913  prmirredlem  21034  psgndiflemB  21145  matsubgcell  21928  tposmap  21951  mat1dim0  21967  mat1dimid  21968  mat1dimscm  21969  mat1dimmul  21970  dmatmul  21991  dmatcrng  21996  scmatcrng  22015  scmatf1  22025  1marepvsma1  22077  maducoeval2  22134  smadiadetlem3lem0  22159  slesolinv  22174  cramerimplem1  22177  cramerimplem2  22178  1pmatscmul  22196  cpmatacl  22210  cpmatmcllem  22212  cpmatmcl  22213  mat2pmatf1  22223  mat2pmatghm  22224  mat2pmatmul  22225  mat2pmatlin  22229  mat2pmatscmxcl  22234  m2cpmmhm  22239  m2pmfzgsumcl  22242  decpmatmul  22266  pmatcollpw2lem  22271  monmatcollpw  22273  pmatcollpwfi  22276  pmatcollpw3fi1lem2  22281  pmatcollpwscmatlem1  22283  pmatcollpwscmatlem2  22284  pmatcollpwscmat  22285  pm2mpghm  22310  pm2mpmhmlem2  22313  pm2mp  22319  chmatcl  22322  chmatval  22323  chmaidscmat  22342  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmulcl  22351  chfacfscmul0  22352  chfacfscmulgsum  22354  chfacfpmmul0  22356  chfacfpmmulgsum  22358  chfacfpmmulgsum2  22359  cayhamlem1  22360  cpmidgsumm2pm  22363  cpmidpmatlem2  22365  cpmadugsumlemB  22368  cpmadugsumlemC  22369  cpmadugsumlemF  22370  cpmadugsumfi  22371  cpmidgsum2  22373  cpmadumatpolylem2  22376  cayhamlem2  22378  chcoeffeqlem  22379  cayleyhamilton0  22383  cayleyhamiltonALT  22385  toponcom  22422  neitr  22676  cnprest  22785  nrmsep2  22852  bwth  22906  2ndcsep  22955  isref  23005  reghaus  23321  isfil2  23352  alexsubALTlem3  23545  cnextcn  23563  lpbl  24004  cmodscmulexp  24630  iscau4  24788  caussi  24806  cmetcusp  24863  ovolicc2lem3  25028  limcresi  25394  elply2  25702  elqaa  25827  aannenlem1  25833  aannenlem2  25834  relogbreexp  26270  cxplogb  26281  bpos1lem  26775  noetalem2  27235  tgjustc1  27716  tgjustc2  27717  axcont  28224  usgrexmplef  28506  subupgr  28534  cplgr3v  28682  cusgrfilem2  28703  usgredgsscusgredg  28706  rusgrprop0  28814  uspgr2wlkeqi  28895  trlontrl  28958  spthonpthon  28998  usgr2wlkspthlem1  29004  usgr2wlkspthlem2  29005  clwlkcompim  29027  clwlkl1loop  29030  wwlksnred  29136  clwwlknonwwlknonb  29349  clwwlknun  29355  1pthon2v  29396  frcond1  29509  frcond4  29513  frgrnbnb  29536  clwlknon2num  29611  numclwlk1lem1  29612  numclwlk1lem2  29613  numclwwlkovh  29616  numclwwlk2lem1  29619  numclwlk2lem2f  29620  numclwwlk2  29624  isgrpo  29738  vcz  29816  hvsub4  30278  hvaddsub4  30319  5oalem2  30896  5oalem5  30899  5oalem6  30900  3oalem2  30904  homcl  30987  hoadddi  31044  stle0i  31480  spansncv2  31534  mdsymlem1  31644  cdj3lem1  31675  f1ocnt  32001  gsumle  32230  gsumvsca1  32359  gsumvsca2  32360  crefdf  32817  sxbrsigalem0  33259  dya2icoseg2  33266  eulerpartlemgvv  33364  ballotlemirc  33519  bnj168  33730  bnj546  33896  bnj594  33912  bnj1097  33981  bnj1110  33982  bnj1174  34003  bnj1176  34005  cusgredgex2  34102  acycgrislfgr  34132  umgracycusgr  34134  cusgracyclt3v  34136  satfv1  34343  satf0suclem  34355  fmlasuc0  34364  fmlafvel  34365  satffunlem2lem1  34384  satfun  34391  fv1stcnv  34737  colineardim1  35022  idinside  35045  finminlem  35192  ivthALT  35209  lukshef-ax2  35289  bj-19.41al  35525  bj-equs45fv  35678  bj-elabd2ALT  35794  bj-rest10b  35959  copsex2b  36010  bj-elid6  36040  bj-ccinftydisj  36083  mptsnunlem  36208  topdifinffinlem  36217  relowlssretop  36233  elxp8  36241  fvineqsnf1  36280  pibt1  36286  matunitlindflem1  36473  poimirlem22  36499  poimirlem25  36502  poimirlem27  36504  poimirlem31  36508  ovoliunnfl  36519  itg2addnclem  36528  sstotbnd3  36633  heibor1lem  36666  heibor1  36667  rngmgmbs4  36788  exmid2  36956  redundss3  37487  redundpim3  37489  dalem53  38585  dalem54  38586  linepsubN  38612  pmapsub  38628  elpaddri  38662  pclfinN  38760  pclcmpatN  38761  cdlemg33c0  39562  dihatexv2  40199  eldioph4i  41536  acongtr  41703  pwfi2f1o  41824  aaitgo  41890  tfsconcat0b  42082  frege54cor0a  42600  clsf2  42863  ismnushort  43046  dvsconst  43075  mptssid  43930  xlimxrre  44534  icccncfext  44590  stoweidlem17  44720  elaa2  44937  dmfcoafv  45870  elfzelfzlble  46016  prprelprb  46172  fmtnoprmfac1  46220  fmtnoprmfac2  46222  flsqrt  46248  lighneallem3  46262  proththd  46269  evenprm2  46369  gbogbow  46411  c0mgm  46694  c0rhm  46697  rhmisrnghm  46708  2zrngnmrid  46802  rhmsubcrngclem1  46879  srhmsubclem1  46925  rhmsubcALTVlem3  46958  linccl  47049  lincvalpr  47053  lincdifsn  47059  lincext1  47089  lindslinindsimp1  47092  ldepspr  47108  lincresunit3lem1  47114  logblt1b  47204  dignnld  47243  dig1  47248  dignn0flhalflem1  47255  itcovalsucov  47308  line  47372  rrxline  47374  rrxsphere  47388  itschlc0xyqsol1  47406  itsclc0xyqsolr  47409  lubeldm2  47543  glbeldm2  47544  amgmwlem  47803