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  2449  equs45f  2461  moaneu  2620  dariiALT  2663  festinoALT  2672  barocoALT  2674  r19.27v  3162  rspc2ev  3586  reu3  3682  difrab  4267  opthprneg  4816  copsexgw  5433  copsexg  5434  imainss  6106  trssord  6328  ordnbtwn  6406  fof  6740  fv3  6846  fvelimab  6900  dff2  7038  dffo5  7043  foco2  7048  fnsnbOLD  7106  tpres  7141  f13dfv  7214  dff1o6  7215  oprabidw  7383  oprabid  7384  ssoprab2i  7463  ndmovass  7540  ndmovdistr  7541  elovmpt3rab1  7612  tfi  7789  find  7831  releldm2  7981  bropopvvv  8026  bropfvvvvlem  8027  ressuppssdif  8121  omlimcl  8499  odi  8500  ixpf  8850  dif1en  9078  domtrfil  9108  funsnfsupp  9283  hartogs  9437  card2on  9447  zfreg  9489  epfrs  9628  acni3  9945  dfac2b  10029  cflm  10148  axdc2lem  10346  ac6s  10382  ondomon  10461  axregndlem1  10500  axregnd  10502  eltsk2g  10649  grothpw  10724  grothpwex  10725  grothomex  10727  ltexprlem1  10934  ltexprlem4  10937  recexsrlem  11001  elfzp12  13505  hashf1rn  14261  hashdifpr  14324  hashgt23el  14333  hashge2el2dif  14389  ccatsymb  14492  swrdnd0  14567  swrdpfx  14616  pfxpfx  14617  pfxccatin12  14642  cshwidxmod  14712  repswcshw  14721  cshimadifsn  14738  cshimadifsn0  14739  pfxco  14747  wwlktovfo  14867  relexpsucnnl  14939  cau3lem  15264  rlimres  15467  dvdsnegb  16186  dvds2add  16203  dvds2sub  16204  nn0onn  16293  gcd2n0cl  16422  lcmfun  16558  divgcdcoprmex  16579  cncongr1  16580  isfunc  17773  drsdirfi  18213  chnrev  18535  sgrpidmnd  18649  smndex1iidm  18811  gaid  19213  symg2bas  19307  qusecsub  19749  gsumle  20059  c0mgm  20379  rhmisrnghm  20400  c0rhm  20451  rhmsubcrngclem1  20583  srhmsubclem1  20594  abvn0b  20753  lmhmlem  20965  prmirredlem  21411  psgndiflemB  21539  ismhp  22056  matsubgcell  22350  tposmap  22373  mat1dim0  22389  mat1dimid  22390  mat1dimscm  22391  mat1dimmul  22392  dmatmul  22413  dmatcrng  22418  scmatcrng  22437  scmatf1  22447  1marepvsma1  22499  maducoeval2  22556  smadiadetlem3lem0  22581  slesolinv  22596  cramerimplem1  22599  cramerimplem2  22600  1pmatscmul  22618  cpmatacl  22632  cpmatmcllem  22634  cpmatmcl  22635  mat2pmatf1  22645  mat2pmatghm  22646  mat2pmatmul  22647  mat2pmatlin  22651  mat2pmatscmxcl  22656  m2cpmmhm  22661  m2pmfzgsumcl  22664  decpmatmul  22688  pmatcollpw2lem  22693  monmatcollpw  22695  pmatcollpwfi  22698  pmatcollpw3fi1lem2  22703  pmatcollpwscmatlem1  22705  pmatcollpwscmatlem2  22706  pmatcollpwscmat  22707  pm2mpghm  22732  pm2mpmhmlem2  22735  pm2mp  22741  chmatcl  22744  chmatval  22745  chmaidscmat  22764  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulcl  22773  chfacfscmul0  22774  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmidgsumm2pm  22785  cpmidpmatlem2  22787  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  cpmadugsumfi  22793  cpmidgsum2  22795  cpmadumatpolylem2  22798  cayhamlem2  22800  chcoeffeqlem  22801  cayleyhamilton0  22805  cayleyhamiltonALT  22807  toponcom  22844  neitr  23096  cnprest  23205  nrmsep2  23272  bwth  23326  2ndcsep  23375  isref  23425  reghaus  23741  isfil2  23772  alexsubALTlem3  23965  cnextcn  23983  lpbl  24419  cmodscmulexp  25050  iscau4  25207  caussi  25225  cmetcusp  25282  ovolicc2lem3  25448  limcresi  25814  elply2  26129  elqaa  26258  aannenlem1  26264  aannenlem2  26265  relogbreexp  26713  cxplogb  26724  bpos1lem  27221  noetalem2  27682  tgjustc1  28454  tgjustc2  28455  axcont  28956  usgrexmplef  29239  subupgr  29267  cplgr3v  29415  cusgrfilem2  29437  usgredgsscusgredg  29440  rusgrprop0  29548  uspgr2wlkeqi  29628  trlontrl  29689  spthonpthon  29731  usgr2wlkspthlem1  29737  usgr2wlkspthlem2  29738  clwlkcompim  29760  clwlkl1loop  29763  wwlksnred  29872  clwwlknonwwlknonb  30088  clwwlknun  30094  1pthon2v  30135  frcond1  30248  frcond4  30252  frgrnbnb  30275  clwlknon2num  30350  numclwlk1lem1  30351  numclwlk1lem2  30352  numclwwlkovh  30355  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwwlk2  30363  isgrpo  30479  vcz  30557  hvsub4  31019  hvaddsub4  31060  5oalem2  31637  5oalem5  31640  5oalem6  31641  3oalem2  31645  homcl  31728  hoadddi  31785  stle0i  32221  spansncv2  32275  mdsymlem1  32385  cdj3lem1  32416  f1ocnt  32787  gsumvsca1  33202  gsumvsca2  33203  crefdf  33882  sxbrsigalem0  34305  dya2icoseg2  34312  eulerpartlemgvv  34410  ballotlemirc  34566  bnj168  34763  bnj546  34929  bnj594  34945  bnj1097  35014  bnj1110  35015  bnj1174  35036  bnj1176  35038  cusgredgex2  35188  acycgrislfgr  35217  umgracycusgr  35219  cusgracyclt3v  35221  satfv1  35428  satf0suclem  35440  fmlasuc0  35449  fmlafvel  35450  satffunlem2lem1  35469  satfun  35476  fv1stcnv  35842  colineardim1  36126  idinside  36149  finminlem  36383  ivthALT  36400  lukshef-ax2  36480  bj-19.41al  36724  bj-equs45fv  36876  bj-elabd2ALT  36990  bj-rest10b  37154  copsex2b  37205  bj-elid6  37235  bj-ccinftydisj  37278  mptsnunlem  37403  topdifinffinlem  37412  relowlssretop  37428  elxp8  37436  fvineqsnf1  37475  pibt1  37481  matunitlindflem1  37676  poimirlem22  37702  poimirlem25  37705  poimirlem27  37707  poimirlem31  37711  ovoliunnfl  37722  itg2addnclem  37731  sstotbnd3  37836  heibor1lem  37869  heibor1  37870  rngmgmbs4  37991  exmid2  38159  redundss3  38744  redundpim3  38746  dalem53  39844  dalem54  39845  linepsubN  39871  pmapsub  39887  elpaddri  39921  pclfinN  40019  pclcmpatN  40020  cdlemg33c0  40821  dihatexv2  41458  eldioph4i  42929  acongtr  43095  pwfi2f1o  43213  aaitgo  43279  tfsconcat0b  43463  frege54cor0a  43980  clsf2  44243  ismnushort  44418  dvsconst  44447  mptssid  45362  xlimxrre  45953  icccncfext  46009  dvmptfprod  46067  stoweidlem17  46139  elaa2  46356  dmfcoafv  47299  elfzelfzlble  47445  prprelprb  47641  fmtnoprmfac1  47689  fmtnoprmfac2  47691  flsqrt  47717  lighneallem3  47731  proththd  47738  evenprm2  47838  gbogbow  47880  clnbgrel  47952  clnbgredg  47964  uhgrimisgrgric  48055  isubgr3stgrlem1  48090  isubgr3stgr  48099  gpg3nbgrvtx0  48200  gpgvtxdg3  48206  2zrngnmrid  48380  rhmsubcALTVlem3  48407  linccl  48539  lincvalpr  48543  lincdifsn  48549  lincext1  48579  lindslinindsimp1  48582  ldepspr  48598  lincresunit3lem1  48604  logblt1b  48689  dignnld  48728  dig1  48733  dignn0flhalflem1  48740  itcovalsucov  48793  line  48857  rrxline  48859  rrxsphere  48873  itschlc0xyqsol1  48891  itsclc0xyqsolr  48894  lubeldm2  49080  glbeldm2  49081  isinito4a  49673  amgmwlem  49927