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  1950  exdistrf  2451  equs45f  2463  moaneu  2623  dariiALT  2666  festinoALT  2675  barocoALT  2677  r19.27v  3165  rspc2ev  3589  reu3  3685  difrab  4270  opthprneg  4821  copsexgw  5438  copsexg  5439  imainss  6112  trssord  6334  ordnbtwn  6412  fof  6746  fv3  6852  fvelimab  6906  dff2  7044  dffo5  7049  foco2  7054  fnsnbOLD  7112  tpres  7147  f13dfv  7220  dff1o6  7221  oprabidw  7389  oprabid  7390  ssoprab2i  7469  ndmovass  7546  ndmovdistr  7547  elovmpt3rab1  7618  tfi  7795  find  7837  releldm2  7987  bropopvvv  8032  bropfvvvvlem  8033  ressuppssdif  8127  omlimcl  8505  odi  8506  ixpf  8858  dif1en  9086  domtrfil  9116  funsnfsupp  9295  hartogs  9449  card2on  9459  zfreg  9501  epfrs  9640  acni3  9957  dfac2b  10041  cflm  10160  axdc2lem  10358  ac6s  10394  ondomon  10473  axregndlem1  10513  axregnd  10515  eltsk2g  10662  grothpw  10737  grothpwex  10738  grothomex  10740  ltexprlem1  10947  ltexprlem4  10950  recexsrlem  11014  elfzp12  13519  hashf1rn  14275  hashdifpr  14338  hashgt23el  14347  hashge2el2dif  14403  ccatsymb  14506  swrdnd0  14581  swrdpfx  14630  pfxpfx  14631  pfxccatin12  14656  cshwidxmod  14726  repswcshw  14735  cshimadifsn  14752  cshimadifsn0  14753  pfxco  14761  wwlktovfo  14881  relexpsucnnl  14953  cau3lem  15278  rlimres  15481  dvdsnegb  16200  dvds2add  16217  dvds2sub  16218  nn0onn  16307  gcd2n0cl  16436  lcmfun  16572  divgcdcoprmex  16593  cncongr1  16594  isfunc  17788  drsdirfi  18228  chnrev  18550  sgrpidmnd  18664  smndex1iidm  18826  gaid  19228  symg2bas  19322  qusecsub  19764  gsumle  20074  c0mgm  20395  rhmisrnghm  20416  c0rhm  20467  rhmsubcrngclem1  20599  srhmsubclem1  20610  abvn0b  20769  lmhmlem  20981  prmirredlem  21427  psgndiflemB  21555  ismhp  22083  matsubgcell  22378  tposmap  22401  mat1dim0  22417  mat1dimid  22418  mat1dimscm  22419  mat1dimmul  22420  dmatmul  22441  dmatcrng  22446  scmatcrng  22465  scmatf1  22475  1marepvsma1  22527  maducoeval2  22584  smadiadetlem3lem0  22609  slesolinv  22624  cramerimplem1  22627  cramerimplem2  22628  1pmatscmul  22646  cpmatacl  22660  cpmatmcllem  22662  cpmatmcl  22663  mat2pmatf1  22673  mat2pmatghm  22674  mat2pmatmul  22675  mat2pmatlin  22679  mat2pmatscmxcl  22684  m2cpmmhm  22689  m2pmfzgsumcl  22692  decpmatmul  22716  pmatcollpw2lem  22721  monmatcollpw  22723  pmatcollpwfi  22726  pmatcollpw3fi1lem2  22731  pmatcollpwscmatlem1  22733  pmatcollpwscmatlem2  22734  pmatcollpwscmat  22735  pm2mpghm  22760  pm2mpmhmlem2  22763  pm2mp  22769  chmatcl  22772  chmatval  22773  chmaidscmat  22792  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmulcl  22801  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmidgsumm2pm  22813  cpmidpmatlem2  22815  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmidgsum2  22823  cpmadumatpolylem2  22826  cayhamlem2  22828  chcoeffeqlem  22829  cayleyhamilton0  22833  cayleyhamiltonALT  22835  toponcom  22872  neitr  23124  cnprest  23233  nrmsep2  23300  bwth  23354  2ndcsep  23403  isref  23453  reghaus  23769  isfil2  23800  alexsubALTlem3  23993  cnextcn  24011  lpbl  24447  cmodscmulexp  25078  iscau4  25235  caussi  25253  cmetcusp  25310  ovolicc2lem3  25476  limcresi  25842  elply2  26157  elqaa  26286  aannenlem1  26292  aannenlem2  26293  relogbreexp  26741  cxplogb  26752  bpos1lem  27249  noetalem2  27710  tgjustc1  28547  tgjustc2  28548  axcont  29049  usgrexmplef  29332  subupgr  29360  cplgr3v  29508  cusgrfilem2  29530  usgredgsscusgredg  29533  rusgrprop0  29641  uspgr2wlkeqi  29721  trlontrl  29782  spthonpthon  29824  usgr2wlkspthlem1  29830  usgr2wlkspthlem2  29831  clwlkcompim  29853  clwlkl1loop  29856  wwlksnred  29965  clwwlknonwwlknonb  30181  clwwlknun  30187  1pthon2v  30228  frcond1  30341  frcond4  30345  frgrnbnb  30368  clwlknon2num  30443  numclwlk1lem1  30444  numclwlk1lem2  30445  numclwwlkovh  30448  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwwlk2  30456  isgrpo  30572  vcz  30650  hvsub4  31112  hvaddsub4  31153  5oalem2  31730  5oalem5  31733  5oalem6  31734  3oalem2  31738  homcl  31821  hoadddi  31878  stle0i  32314  spansncv2  32368  mdsymlem1  32478  cdj3lem1  32509  f1ocnt  32880  gsumvsca1  33308  gsumvsca2  33309  crefdf  34005  sxbrsigalem0  34428  dya2icoseg2  34435  eulerpartlemgvv  34533  ballotlemirc  34689  bnj168  34886  bnj546  35052  bnj594  35068  bnj1097  35137  bnj1110  35138  bnj1174  35159  bnj1176  35161  cusgredgex2  35317  acycgrislfgr  35346  umgracycusgr  35348  cusgracyclt3v  35350  satfv1  35557  satf0suclem  35569  fmlasuc0  35578  fmlafvel  35579  satffunlem2lem1  35598  satfun  35605  fv1stcnv  35971  colineardim1  36255  idinside  36278  finminlem  36512  ivthALT  36529  lukshef-ax2  36609  exeltr  36665  regsfromregtr  36668  bj-19.41al  36860  bj-equs45fv  37012  bj-elabd2ALT  37126  bj-rest10b  37290  copsex2b  37341  bj-elid6  37371  bj-ccinftydisj  37414  mptsnunlem  37539  topdifinffinlem  37548  relowlssretop  37564  elxp8  37572  fvineqsnf1  37611  pibt1  37617  matunitlindflem1  37813  poimirlem22  37839  poimirlem25  37842  poimirlem27  37844  poimirlem31  37848  ovoliunnfl  37859  itg2addnclem  37868  sstotbnd3  37973  heibor1lem  38006  heibor1  38007  rngmgmbs4  38128  exmid2  38296  redundss3  38881  redundpim3  38883  dalem53  39981  dalem54  39982  linepsubN  40008  pmapsub  40024  elpaddri  40058  pclfinN  40156  pclcmpatN  40157  cdlemg33c0  40958  dihatexv2  41595  eldioph4i  43050  acongtr  43216  pwfi2f1o  43334  aaitgo  43400  tfsconcat0b  43584  frege54cor0a  44100  clsf2  44363  ismnushort  44538  dvsconst  44567  mptssid  45481  xlimxrre  46071  icccncfext  46127  dvmptfprod  46185  stoweidlem17  46257  elaa2  46474  dmfcoafv  47417  elfzelfzlble  47563  prprelprb  47759  fmtnoprmfac1  47807  fmtnoprmfac2  47809  flsqrt  47835  lighneallem3  47849  proththd  47856  evenprm2  47956  gbogbow  47998  clnbgrel  48070  clnbgredg  48082  uhgrimisgrgric  48173  isubgr3stgrlem1  48208  isubgr3stgr  48217  gpg3nbgrvtx0  48318  gpgvtxdg3  48324  2zrngnmrid  48498  rhmsubcALTVlem3  48525  linccl  48656  lincvalpr  48660  lincdifsn  48666  lincext1  48696  lindslinindsimp1  48699  ldepspr  48715  lincresunit3lem1  48721  logblt1b  48806  dignnld  48845  dig1  48850  dignn0flhalflem1  48857  itcovalsucov  48910  line  48974  rrxline  48976  rrxsphere  48990  itschlc0xyqsol1  49008  itsclc0xyqsolr  49011  lubeldm2  49197  glbeldm2  49198  isinito4a  49789  amgmwlem  50043