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 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  684  andi  1010  19.41v  1951  exdistrf  2451  equs45f  2463  moaneu  2623  dariiALT  2666  festinoALT  2675  barocoALT  2677  r19.27v  3166  rspc2ev  3577  reu3  3673  difrab  4258  opthprneg  4808  copsexgwOLD  5444  copsexg  5445  imainss  6118  trssord  6340  ordnbtwn  6418  fof  6752  fv3  6858  fvelimab  6912  dff2  7051  dffo5  7056  foco2  7061  fnsnbOLD  7121  tpres  7156  f13dfv  7229  dff1o6  7230  oprabidw  7398  oprabid  7399  ssoprab2i  7478  ndmovass  7555  ndmovdistr  7556  elovmpt3rab1  7627  tfi  7804  find  7846  releldm2  7996  bropopvvv  8040  bropfvvvvlem  8041  ressuppssdif  8135  omlimcl  8513  odi  8514  ixpf  8868  dif1en  9096  domtrfil  9126  funsnfsupp  9305  hartogs  9459  card2on  9469  zfreg  9511  epfrs  9652  acni3  9969  dfac2b  10053  cflm  10172  axdc2lem  10370  ac6s  10406  ondomon  10485  axregndlem1  10525  axregnd  10527  eltsk2g  10674  grothpw  10749  grothpwex  10750  grothomex  10752  ltexprlem1  10959  ltexprlem4  10962  recexsrlem  11026  elfzp12  13557  hashf1rn  14314  hashdifpr  14377  hashgt23el  14386  hashge2el2dif  14442  ccatsymb  14545  swrdnd0  14620  swrdpfx  14669  pfxpfx  14670  pfxccatin12  14695  cshwidxmod  14765  repswcshw  14774  cshimadifsn  14791  cshimadifsn0  14792  pfxco  14800  wwlktovfo  14920  relexpsucnnl  14992  cau3lem  15317  rlimres  15520  dvdsnegb  16242  dvds2add  16259  dvds2sub  16260  nn0onn  16349  gcd2n0cl  16478  lcmfun  16614  divgcdcoprmex  16635  cncongr1  16636  isfunc  17831  drsdirfi  18271  chnrev  18593  sgrpidmnd  18707  smndex1iidm  18869  gaid  19274  symg2bas  19368  qusecsub  19810  gsumle  20120  c0mgm  20439  rhmisrnghm  20460  c0rhm  20511  rhmsubcrngclem1  20643  srhmsubclem1  20654  abvn0b  20813  lmhmlem  21024  prmirredlem  21452  psgndiflemB  21580  ismhp  22106  matsubgcell  22399  tposmap  22422  mat1dim0  22438  mat1dimid  22439  mat1dimscm  22440  mat1dimmul  22441  dmatmul  22462  dmatcrng  22467  scmatcrng  22486  scmatf1  22496  1marepvsma1  22548  maducoeval2  22605  smadiadetlem3lem0  22630  slesolinv  22645  cramerimplem1  22648  cramerimplem2  22649  1pmatscmul  22667  cpmatacl  22681  cpmatmcllem  22683  cpmatmcl  22684  mat2pmatf1  22694  mat2pmatghm  22695  mat2pmatmul  22696  mat2pmatlin  22700  mat2pmatscmxcl  22705  m2cpmmhm  22710  m2pmfzgsumcl  22713  decpmatmul  22737  pmatcollpw2lem  22742  monmatcollpw  22744  pmatcollpwfi  22747  pmatcollpw3fi1lem2  22752  pmatcollpwscmatlem1  22754  pmatcollpwscmatlem2  22755  pmatcollpwscmat  22756  pm2mpghm  22781  pm2mpmhmlem2  22784  pm2mp  22790  chmatcl  22793  chmatval  22794  chmaidscmat  22813  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulcl  22822  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmidgsumm2pm  22834  cpmidpmatlem2  22836  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmidgsum2  22844  cpmadumatpolylem2  22847  cayhamlem2  22849  chcoeffeqlem  22850  cayleyhamilton0  22854  cayleyhamiltonALT  22856  toponcom  22893  neitr  23145  cnprest  23254  nrmsep2  23321  bwth  23375  2ndcsep  23424  isref  23474  reghaus  23790  isfil2  23821  alexsubALTlem3  24014  cnextcn  24032  lpbl  24468  cmodscmulexp  25089  iscau4  25246  caussi  25264  cmetcusp  25321  ovolicc2lem3  25486  limcresi  25852  elply2  26161  elqaa  26288  aannenlem1  26294  aannenlem2  26295  relogbreexp  26739  cxplogb  26750  bpos1lem  27245  noetalem2  27706  tgjustc1  28543  tgjustc2  28544  axcont  29045  usgrexmplef  29328  subupgr  29356  cplgr3v  29504  cusgrfilem2  29525  usgredgsscusgredg  29528  rusgrprop0  29636  uspgr2wlkeqi  29716  trlontrl  29777  spthonpthon  29819  usgr2wlkspthlem1  29825  usgr2wlkspthlem2  29826  clwlkcompim  29848  clwlkl1loop  29851  wwlksnred  29960  clwwlknonwwlknonb  30176  clwwlknun  30182  1pthon2v  30223  frcond1  30336  frcond4  30340  frgrnbnb  30363  clwlknon2num  30438  numclwlk1lem1  30439  numclwlk1lem2  30440  numclwwlkovh  30443  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwwlk2  30451  isgrpo  30568  vcz  30646  hvsub4  31108  hvaddsub4  31149  5oalem2  31726  5oalem5  31729  5oalem6  31730  3oalem2  31734  homcl  31817  hoadddi  31874  stle0i  32310  spansncv2  32364  mdsymlem1  32474  cdj3lem1  32505  f1ocnt  32873  gsumvsca1  33287  gsumvsca2  33288  crefdf  33992  sxbrsigalem0  34415  dya2icoseg2  34422  eulerpartlemgvv  34520  ballotlemirc  34676  bnj168  34873  bnj546  35038  bnj594  35054  bnj1097  35123  bnj1110  35124  bnj1174  35145  bnj1176  35147  axprALT2  35253  cusgredgex2  35305  acycgrislfgr  35334  umgracycusgr  35336  cusgracyclt3v  35338  satfv1  35545  satf0suclem  35557  fmlasuc0  35566  fmlafvel  35567  satffunlem2lem1  35586  satfun  35593  fv1stcnv  35959  colineardim1  36243  idinside  36266  finminlem  36500  ivthALT  36517  lukshef-ax2  36597  regsfromregtco  36720  bj-19.41al  36953  bj-equs45fv  37118  bj-elabd2ALT  37232  bj-rest10b  37401  copsex2b  37454  bj-elid6  37484  bj-ccinftydisj  37527  mptsnunlem  37654  topdifinffinlem  37663  relowlssretop  37679  elxp8  37687  fvineqsnf1  37726  pibt1  37732  matunitlindflem1  37937  poimirlem22  37963  poimirlem25  37966  poimirlem27  37968  poimirlem31  37972  ovoliunnfl  37983  itg2addnclem  37992  sstotbnd3  38097  heibor1lem  38130  heibor1  38131  rngmgmbs4  38252  exmid2  38420  redundss3  39033  redundpim3  39035  dalem53  40171  dalem54  40172  linepsubN  40198  pmapsub  40214  elpaddri  40248  pclfinN  40346  pclcmpatN  40347  cdlemg33c0  41148  dihatexv2  41785  eldioph4i  43240  acongtr  43406  pwfi2f1o  43524  aaitgo  43590  tfsconcat0b  43774  frege54cor0a  44290  clsf2  44553  ismnushort  44728  dvsconst  44757  mptssid  45670  xlimxrre  46259  icccncfext  46315  dvmptfprod  46373  stoweidlem17  46445  elaa2  46662  dmfcoafv  47623  elfzelfzlble  47769  prprelprb  47977  fmtnoprmfac1  48028  fmtnoprmfac2  48030  flsqrt  48056  lighneallem3  48070  proththd  48077  evenprm2  48190  gbogbow  48232  clnbgrel  48304  clnbgredg  48316  uhgrimisgrgric  48407  isubgr3stgrlem1  48442  isubgr3stgr  48451  gpg3nbgrvtx0  48552  gpgvtxdg3  48558  2zrngnmrid  48732  rhmsubcALTVlem3  48759  linccl  48890  lincvalpr  48894  lincdifsn  48900  lincext1  48930  lindslinindsimp1  48933  ldepspr  48949  lincresunit3lem1  48955  logblt1b  49040  dignnld  49079  dig1  49084  dignn0flhalflem1  49091  itcovalsucov  49144  line  49208  rrxline  49210  rrxsphere  49224  itschlc0xyqsol1  49242  itsclc0xyqsolr  49245  lubeldm2  49431  glbeldm2  49432  isinito4a  50023  amgmwlem  50277