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 398

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 209  df-an 399

This theorem is referenced by:  sylanr2  681  andi  1004  19.41v  1949  exdistrf  2468  equs45f  2481  sbimiOLD  2514  sbimiALT  2576  moaneu  2707  dariiALT  2752  festinoALT  2761  barocoALT  2763  r19.27v  3187  r19.27vOLD  3188  rspc2ev  3638  reu3  3721  difrab  4280  opthprneg  4798  copsexgw  5384  copsexg  5385  imainss  6014  trssord  6211  ordnbtwn  6284  fof  6593  fv3  6691  fvelimab  6740  dff2  6868  dffo5  6873  foco2  6876  fnsnb  6931  tpres  6966  f13dfv  7034  dff1o6  7035  oprabidw  7190  oprabid  7191  ssoprab2i  7266  ndmovass  7339  ndmovdistr  7340  elovmpt3rab1  7408  tfi  7571  find  7610  releldm2  7745  bropopvvv  7788  bropfvvvvlem  7789  ressuppssdif  7854  supp0cosupp0OLD  7876  imacosuppOLD  7878  omlimcl  8207  odi  8208  ixpf  8487  funsnfsupp  8860  hartogs  9011  card2on  9021  zfreg  9062  epfrs  9176  acni3  9476  dfac2b  9559  cflm  9675  axdc2lem  9873  ac6s  9909  ondomon  9988  axregndlem1  10027  axregnd  10029  eltsk2g  10176  grothpw  10251  grothpwex  10252  grothomex  10254  ltexprlem1  10461  ltexprlem4  10464  recexsrlem  10528  elfzp12  12989  focdmex  13714  hashf1rn  13716  hashdifpr  13779  hashgt23el  13788  hashge2el2dif  13841  ccatsymb  13939  swrdnd0  14022  swrdpfx  14072  pfxpfx  14073  pfxccatin12  14098  cshwidxmod  14168  repswcshw  14177  cshimadifsn  14194  cshimadifsn0  14195  pfxco  14203  wwlktovfo  14325  relexpsucnnl  14394  cau3lem  14717  rlimres  14918  dvdsnegb  15630  dvds2add  15646  dvds2sub  15647  nn0onn  15734  gcd2n0cl  15861  lcmfun  15992  divgcdcoprmex  16013  cncongr1  16014  isfunc  17137  drsdirfi  17551  sgrpidmnd  17919  smndex1iidm  18069  gaid  18432  symg2bas  18524  lmhmlem  19804  abvn0b  20078  prmirredlem  20643  psgndiflemB  20747  matsubgcell  21046  tposmap  21069  mat1dim0  21085  mat1dimid  21086  mat1dimscm  21087  mat1dimmul  21088  dmatmul  21109  dmatcrng  21114  scmatcrng  21133  scmatf1  21143  1marepvsma1  21195  maducoeval2  21252  smadiadetlem3lem0  21277  slesolinv  21292  cramerimplem1  21295  cramerimplem2  21296  1pmatscmul  21313  cpmatacl  21327  cpmatmcllem  21329  cpmatmcl  21330  mat2pmatf1  21340  mat2pmatghm  21341  mat2pmatmul  21342  mat2pmatlin  21346  mat2pmatscmxcl  21351  m2cpmmhm  21356  m2pmfzgsumcl  21359  m2cpmrngiso  21369  decpmatmul  21383  pmatcollpw2lem  21388  monmatcollpw  21390  pmatcollpwfi  21393  pmatcollpw3fi1lem2  21398  pmatcollpwscmatlem1  21400  pmatcollpwscmatlem2  21401  pmatcollpwscmat  21402  pm2mpghm  21427  pm2mpmhmlem2  21430  pm2mp  21436  chmatcl  21439  chmatval  21440  chmaidscmat  21459  chfacfisf  21465  chfacfisfcpmat  21466  chfacfscmulcl  21468  chfacfscmul0  21469  chfacfscmulgsum  21471  chfacfpmmul0  21473  chfacfpmmulgsum  21475  chfacfpmmulgsum2  21476  cayhamlem1  21477  cpmidgsumm2pm  21480  cpmidpmatlem2  21482  cpmadugsumlemB  21485  cpmadugsumlemC  21486  cpmadugsumlemF  21487  cpmadugsumfi  21488  cpmidgsum2  21490  cpmadumatpolylem2  21493  cayhamlem2  21495  chcoeffeqlem  21496  cayleyhamilton0  21500  cayleyhamiltonALT  21502  toponcom  21539  neitr  21791  cnprest  21900  nrmsep2  21967  bwth  22021  2ndcsep  22070  isref  22120  reghaus  22436  isfil2  22467  alexsubALTlem3  22660  cnextcn  22678  lpbl  23116  cmodscmulexp  23729  iscau4  23885  caussi  23903  cmetcusp  23960  ovolicc2lem3  24123  limcresi  24486  elply2  24789  elqaa  24914  aannenlem1  24920  aannenlem2  24921  relogbreexp  25356  cxplogb  25367  bpos1lem  25861  tgjustc1  26264  tgjustc2  26265  axcont  26765  usgrexmplef  27044  subupgr  27072  cplgr3v  27220  cusgrfilem2  27241  usgredgsscusgredg  27244  rusgrprop0  27352  uspgr2wlkeqi  27432  trlontrl  27495  spthonpthon  27535  usgr2wlkspthlem1  27541  usgr2wlkspthlem2  27542  clwlkcompim  27564  clwlkl1loop  27567  wwlksnred  27673  wwlksnfiOLD  27688  clwwlknonwwlknonb  27888  clwwlknun  27894  1pthon2v  27935  frcond1  28048  frcond4  28052  frgrnbnb  28075  clwlknon2num  28150  numclwlk1lem1  28151  numclwlk1lem2  28152  numclwwlkovh  28155  numclwwlk2lem1  28158  numclwlk2lem2f  28159  numclwwlk2  28163  isgrpo  28277  vcz  28355  hvsub4  28817  hvaddsub4  28858  5oalem2  29435  5oalem5  29438  5oalem6  29439  3oalem2  29443  homcl  29526  hoadddi  29583  stle0i  30019  spansncv2  30073  mdsymlem1  30183  cdj3lem1  30214  f1ocnt  30528  gsumle  30729  gsumvsca1  30858  gsumvsca2  30859  crefdf  31116  sxbrsigalem0  31533  dya2icoseg2  31540  eulerpartlemgvv  31638  ballotlemirc  31793  bnj168  32004  bnj546  32172  bnj594  32188  bnj1097  32257  bnj1110  32258  bnj1174  32279  bnj1176  32281  cusgredgex2  32373  acycgrislfgr  32403  umgracycusgr  32405  cusgracyclt3v  32407  satfv1  32614  satf0suclem  32626  fmlasuc0  32635  fmlafvel  32636  satffunlem2lem1  32655  satfun  32662  fv1stcnv  33024  noetalem5  33225  colineardim1  33526  idinside  33549  finminlem  33670  ivthALT  33687  lukshef-ax2  33767  bj-19.41al  33996  bj-equs45fv  34137  bj-rest10b  34384  copsex2b  34436  bj-elid6  34466  bj-ccinftydisj  34499  mptsnunlem  34623  topdifinffinlem  34632  relowlssretop  34648  elxp8  34656  fvineqsnf1  34695  pibt1  34701  matunitlindflem1  34892  poimirlem22  34918  poimirlem25  34921  poimirlem27  34923  poimirlem31  34927  ovoliunnfl  34938  itg2addnclem  34947  sstotbnd3  35058  heibor1lem  35091  heibor1  35092  rngmgmbs4  35213  exmid2  35381  redundss3  35867  redundpim3  35869  dalem53  36865  dalem54  36866  linepsubN  36892  pmapsub  36908  elpaddri  36942  pclfinN  37040  pclcmpatN  37041  cdlemg33c0  37842  dihatexv2  38479  eldioph4i  39415  acongtr  39581  pwfi2f1o  39702  aaitgo  39768  frege54cor0a  40215  clsf2  40482  dvsconst  40668  mptssid  41517  xlimxrre  42118  icccncfext  42176  stoweidlem17  42309  elaa2  42526  dmfcoafv  43381  elfzelfzlble  43528  prprelprb  43686  fmtnoprmfac1  43734  fmtnoprmfac2  43736  flsqrt  43763  lighneallem3  43779  proththd  43786  evenprm2  43886  gbogbow  43928  uspgrsprfo  44030  c0mgm  44187  c0rhm  44190  rhmisrnghm  44198  lidlmmgm  44203  2zrngnmrid  44228  rhmsubcrngclem1  44305  srhmsubclem1  44351  rhmsubcALTVlem3  44384  linccl  44476  lincvalpr  44480  lincdifsn  44486  lincext1  44516  lindslinindsimp1  44519  ldepspr  44535  lincresunit3lem1  44541  logblt1b  44631  dignnld  44670  dig1  44675  dignn0flhalflem1  44682  line  44726  rrxline  44728  rrxsphere  44742  itschlc0xyqsol1  44760  itsclc0xyqsolr  44763  amgmwlem  44910