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  1949  exdistrf  2445  equs45f  2457  moaneu  2616  dariiALT  2659  festinoALT  2668  barocoALT  2670  r19.27v  3158  rspc2ev  3592  reu3  3689  difrab  4271  opthprneg  4819  copsexgw  5437  copsexg  5438  imainss  6107  trssord  6328  ordnbtwn  6406  fof  6740  fv3  6844  fvelimab  6899  dff2  7037  dffo5  7042  foco2  7047  fnsnbOLD  7106  tpres  7141  f13dfv  7215  dff1o6  7216  oprabidw  7384  oprabid  7385  ssoprab2i  7464  ndmovass  7541  ndmovdistr  7542  elovmpt3rab1  7613  tfi  7793  find  7835  releldm2  7985  bropopvvv  8030  bropfvvvvlem  8031  ressuppssdif  8125  omlimcl  8503  odi  8504  ixpf  8854  dif1en  9084  domtrfil  9116  funsnfsupp  9301  hartogs  9455  card2on  9465  zfreg  9507  epfrs  9646  acni3  9960  dfac2b  10044  cflm  10163  axdc2lem  10361  ac6s  10397  ondomon  10476  axregndlem1  10515  axregnd  10517  eltsk2g  10664  grothpw  10739  grothpwex  10740  grothomex  10742  ltexprlem1  10949  ltexprlem4  10952  recexsrlem  11016  elfzp12  13524  hashf1rn  14277  hashdifpr  14340  hashgt23el  14349  hashge2el2dif  14405  ccatsymb  14507  swrdnd0  14582  swrdpfx  14631  pfxpfx  14632  pfxccatin12  14657  cshwidxmod  14727  repswcshw  14736  cshimadifsn  14754  cshimadifsn0  14755  pfxco  14763  wwlktovfo  14883  relexpsucnnl  14955  cau3lem  15280  rlimres  15483  dvdsnegb  16202  dvds2add  16219  dvds2sub  16220  nn0onn  16309  gcd2n0cl  16438  lcmfun  16574  divgcdcoprmex  16595  cncongr1  16596  isfunc  17789  drsdirfi  18229  sgrpidmnd  18631  smndex1iidm  18793  gaid  19196  symg2bas  19290  qusecsub  19732  gsumle  20042  c0mgm  20362  rhmisrnghm  20383  c0rhm  20437  rhmsubcrngclem1  20569  srhmsubclem1  20580  abvn0b  20739  lmhmlem  20951  prmirredlem  21397  psgndiflemB  21525  ismhp  22043  matsubgcell  22337  tposmap  22360  mat1dim0  22376  mat1dimid  22377  mat1dimscm  22378  mat1dimmul  22379  dmatmul  22400  dmatcrng  22405  scmatcrng  22424  scmatf1  22434  1marepvsma1  22486  maducoeval2  22543  smadiadetlem3lem0  22568  slesolinv  22583  cramerimplem1  22586  cramerimplem2  22587  1pmatscmul  22605  cpmatacl  22619  cpmatmcllem  22621  cpmatmcl  22622  mat2pmatf1  22632  mat2pmatghm  22633  mat2pmatmul  22634  mat2pmatlin  22638  mat2pmatscmxcl  22643  m2cpmmhm  22648  m2pmfzgsumcl  22651  decpmatmul  22675  pmatcollpw2lem  22680  monmatcollpw  22682  pmatcollpwfi  22685  pmatcollpw3fi1lem2  22690  pmatcollpwscmatlem1  22692  pmatcollpwscmatlem2  22693  pmatcollpwscmat  22694  pm2mpghm  22719  pm2mpmhmlem2  22722  pm2mp  22728  chmatcl  22731  chmatval  22732  chmaidscmat  22751  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulcl  22760  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmidgsumm2pm  22772  cpmidpmatlem2  22774  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cpmadugsumfi  22780  cpmidgsum2  22782  cpmadumatpolylem2  22785  cayhamlem2  22787  chcoeffeqlem  22788  cayleyhamilton0  22792  cayleyhamiltonALT  22794  toponcom  22831  neitr  23083  cnprest  23192  nrmsep2  23259  bwth  23313  2ndcsep  23362  isref  23412  reghaus  23728  isfil2  23759  alexsubALTlem3  23952  cnextcn  23970  lpbl  24407  cmodscmulexp  25038  iscau4  25195  caussi  25213  cmetcusp  25270  ovolicc2lem3  25436  limcresi  25802  elply2  26117  elqaa  26246  aannenlem1  26252  aannenlem2  26253  relogbreexp  26701  cxplogb  26712  bpos1lem  27209  noetalem2  27670  tgjustc1  28438  tgjustc2  28439  axcont  28939  usgrexmplef  29222  subupgr  29250  cplgr3v  29398  cusgrfilem2  29420  usgredgsscusgredg  29423  rusgrprop0  29531  uspgr2wlkeqi  29611  trlontrl  29672  spthonpthon  29714  usgr2wlkspthlem1  29720  usgr2wlkspthlem2  29721  clwlkcompim  29743  clwlkl1loop  29746  wwlksnred  29855  clwwlknonwwlknonb  30068  clwwlknun  30074  1pthon2v  30115  frcond1  30228  frcond4  30232  frgrnbnb  30255  clwlknon2num  30330  numclwlk1lem1  30331  numclwlk1lem2  30332  numclwwlkovh  30335  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwwlk2  30343  isgrpo  30459  vcz  30537  hvsub4  30999  hvaddsub4  31040  5oalem2  31617  5oalem5  31620  5oalem6  31621  3oalem2  31625  homcl  31708  hoadddi  31765  stle0i  32201  spansncv2  32255  mdsymlem1  32365  cdj3lem1  32396  f1ocnt  32758  gsumvsca1  33178  gsumvsca2  33179  crefdf  33814  sxbrsigalem0  34238  dya2icoseg2  34245  eulerpartlemgvv  34343  ballotlemirc  34499  bnj168  34696  bnj546  34862  bnj594  34878  bnj1097  34947  bnj1110  34948  bnj1174  34969  bnj1176  34971  cusgredgex2  35095  acycgrislfgr  35124  umgracycusgr  35126  cusgracyclt3v  35128  satfv1  35335  satf0suclem  35347  fmlasuc0  35356  fmlafvel  35357  satffunlem2lem1  35376  satfun  35383  fv1stcnv  35749  colineardim1  36034  idinside  36057  finminlem  36291  ivthALT  36308  lukshef-ax2  36388  bj-19.41al  36632  bj-equs45fv  36784  bj-elabd2ALT  36898  bj-rest10b  37062  copsex2b  37113  bj-elid6  37143  bj-ccinftydisj  37186  mptsnunlem  37311  topdifinffinlem  37320  relowlssretop  37336  elxp8  37344  fvineqsnf1  37383  pibt1  37389  matunitlindflem1  37595  poimirlem22  37621  poimirlem25  37624  poimirlem27  37626  poimirlem31  37630  ovoliunnfl  37641  itg2addnclem  37650  sstotbnd3  37755  heibor1lem  37788  heibor1  37789  rngmgmbs4  37910  exmid2  38078  redundss3  38604  redundpim3  38606  dalem53  39704  dalem54  39705  linepsubN  39731  pmapsub  39747  elpaddri  39781  pclfinN  39879  pclcmpatN  39880  cdlemg33c0  40681  dihatexv2  41318  eldioph4i  42785  acongtr  42951  pwfi2f1o  43069  aaitgo  43135  tfsconcat0b  43319  frege54cor0a  43836  clsf2  44099  ismnushort  44274  dvsconst  44303  mptssid  45219  xlimxrre  45813  icccncfext  45869  dvmptfprod  45927  stoweidlem17  45999  elaa2  46216  dmfcoafv  47160  elfzelfzlble  47306  prprelprb  47502  fmtnoprmfac1  47550  fmtnoprmfac2  47552  flsqrt  47578  lighneallem3  47592  proththd  47599  evenprm2  47699  gbogbow  47741  clnbgrel  47813  clnbgredg  47825  uhgrimisgrgric  47916  isubgr3stgrlem1  47951  isubgr3stgr  47960  gpg3nbgrvtx0  48061  gpgvtxdg3  48067  2zrngnmrid  48241  rhmsubcALTVlem3  48268  linccl  48400  lincvalpr  48404  lincdifsn  48410  lincext1  48440  lindslinindsimp1  48443  ldepspr  48459  lincresunit3lem1  48465  logblt1b  48550  dignnld  48589  dig1  48594  dignn0flhalflem1  48601  itcovalsucov  48654  line  48718  rrxline  48720  rrxsphere  48734  itschlc0xyqsol1  48752  itsclc0xyqsolr  48755  lubeldm2  48941  glbeldm2  48942  isinito4a  49534  amgmwlem  49788