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  2452  equs45f  2464  moaneu  2623  dariiALT  2666  festinoALT  2675  barocoALT  2677  r19.27v  3174  rspc2ev  3619  reu3  3715  difrab  4298  opthprneg  4846  copsexgw  5470  copsexg  5471  imainss  6148  trssord  6374  ordnbtwn  6452  fof  6795  fv3  6899  fvelimab  6956  dff2  7094  dffo5  7099  foco2  7104  fnsnbOLD  7163  tpres  7198  f13dfv  7272  dff1o6  7273  oprabidw  7441  oprabid  7442  ssoprab2i  7523  ndmovass  7600  ndmovdistr  7601  elovmpt3rab1  7672  tfi  7853  find  7896  releldm2  8047  bropopvvv  8094  bropfvvvvlem  8095  ressuppssdif  8189  omlimcl  8595  odi  8596  ixpf  8939  dif1en  9179  domtrfil  9211  funsnfsupp  9409  hartogs  9563  card2on  9573  zfreg  9614  epfrs  9750  acni3  10066  dfac2b  10150  cflm  10269  axdc2lem  10467  ac6s  10503  ondomon  10582  axregndlem1  10621  axregnd  10623  eltsk2g  10770  grothpw  10845  grothpwex  10846  grothomex  10848  ltexprlem1  11055  ltexprlem4  11058  recexsrlem  11122  elfzp12  13625  hashf1rn  14375  hashdifpr  14438  hashgt23el  14447  hashge2el2dif  14503  ccatsymb  14605  swrdnd0  14680  swrdpfx  14730  pfxpfx  14731  pfxccatin12  14756  cshwidxmod  14826  repswcshw  14835  cshimadifsn  14853  cshimadifsn0  14854  pfxco  14862  wwlktovfo  14982  relexpsucnnl  15054  cau3lem  15378  rlimres  15579  dvdsnegb  16298  dvds2add  16314  dvds2sub  16315  nn0onn  16404  gcd2n0cl  16533  lcmfun  16669  divgcdcoprmex  16690  cncongr1  16691  isfunc  17882  drsdirfi  18322  sgrpidmnd  18722  smndex1iidm  18884  gaid  19287  symg2bas  19379  qusecsub  19821  c0mgm  20424  rhmisrnghm  20445  c0rhm  20499  rhmsubcrngclem1  20631  srhmsubclem1  20642  abvn0b  20801  lmhmlem  20992  prmirredlem  21438  psgndiflemB  21565  ismhp  22083  matsubgcell  22377  tposmap  22400  mat1dim0  22416  mat1dimid  22417  mat1dimscm  22418  mat1dimmul  22419  dmatmul  22440  dmatcrng  22445  scmatcrng  22464  scmatf1  22474  1marepvsma1  22526  maducoeval2  22583  smadiadetlem3lem0  22608  slesolinv  22623  cramerimplem1  22626  cramerimplem2  22627  1pmatscmul  22645  cpmatacl  22659  cpmatmcllem  22661  cpmatmcl  22662  mat2pmatf1  22672  mat2pmatghm  22673  mat2pmatmul  22674  mat2pmatlin  22678  mat2pmatscmxcl  22683  m2cpmmhm  22688  m2pmfzgsumcl  22691  decpmatmul  22715  pmatcollpw2lem  22720  monmatcollpw  22722  pmatcollpwfi  22725  pmatcollpw3fi1lem2  22730  pmatcollpwscmatlem1  22732  pmatcollpwscmatlem2  22733  pmatcollpwscmat  22734  pm2mpghm  22759  pm2mpmhmlem2  22762  pm2mp  22768  chmatcl  22771  chmatval  22772  chmaidscmat  22791  chfacfisf  22797  chfacfisfcpmat  22798  chfacfscmulcl  22800  chfacfscmul0  22801  chfacfscmulgsum  22803  chfacfpmmul0  22805  chfacfpmmulgsum  22807  chfacfpmmulgsum2  22808  cayhamlem1  22809  cpmidgsumm2pm  22812  cpmidpmatlem2  22814  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  cpmadugsumfi  22820  cpmidgsum2  22822  cpmadumatpolylem2  22825  cayhamlem2  22827  chcoeffeqlem  22828  cayleyhamilton0  22832  cayleyhamiltonALT  22834  toponcom  22871  neitr  23123  cnprest  23232  nrmsep2  23299  bwth  23353  2ndcsep  23402  isref  23452  reghaus  23768  isfil2  23799  alexsubALTlem3  23992  cnextcn  24010  lpbl  24447  cmodscmulexp  25078  iscau4  25236  caussi  25254  cmetcusp  25311  ovolicc2lem3  25477  limcresi  25843  elply2  26158  elqaa  26287  aannenlem1  26293  aannenlem2  26294  relogbreexp  26742  cxplogb  26753  bpos1lem  27250  noetalem2  27711  tgjustc1  28459  tgjustc2  28460  axcont  28960  usgrexmplef  29243  subupgr  29271  cplgr3v  29419  cusgrfilem2  29441  usgredgsscusgredg  29444  rusgrprop0  29552  uspgr2wlkeqi  29633  trlontrl  29696  spthonpthon  29738  usgr2wlkspthlem1  29744  usgr2wlkspthlem2  29745  clwlkcompim  29767  clwlkl1loop  29770  wwlksnred  29879  clwwlknonwwlknonb  30092  clwwlknun  30098  1pthon2v  30139  frcond1  30252  frcond4  30256  frgrnbnb  30279  clwlknon2num  30354  numclwlk1lem1  30355  numclwlk1lem2  30356  numclwwlkovh  30359  numclwwlk2lem1  30362  numclwlk2lem2f  30363  numclwwlk2  30367  isgrpo  30483  vcz  30561  hvsub4  31023  hvaddsub4  31064  5oalem2  31641  5oalem5  31644  5oalem6  31645  3oalem2  31649  homcl  31732  hoadddi  31789  stle0i  32225  spansncv2  32279  mdsymlem1  32389  cdj3lem1  32420  f1ocnt  32784  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  crefdf  33884  sxbrsigalem0  34308  dya2icoseg2  34315  eulerpartlemgvv  34413  ballotlemirc  34569  bnj168  34766  bnj546  34932  bnj594  34948  bnj1097  35017  bnj1110  35018  bnj1174  35039  bnj1176  35041  cusgredgex2  35150  acycgrislfgr  35179  umgracycusgr  35181  cusgracyclt3v  35183  satfv1  35390  satf0suclem  35402  fmlasuc0  35411  fmlafvel  35412  satffunlem2lem1  35431  satfun  35438  fv1stcnv  35799  colineardim1  36084  idinside  36107  finminlem  36341  ivthALT  36358  lukshef-ax2  36438  bj-19.41al  36682  bj-equs45fv  36834  bj-elabd2ALT  36948  bj-rest10b  37112  copsex2b  37163  bj-elid6  37193  bj-ccinftydisj  37236  mptsnunlem  37361  topdifinffinlem  37370  relowlssretop  37386  elxp8  37394  fvineqsnf1  37433  pibt1  37439  matunitlindflem1  37645  poimirlem22  37671  poimirlem25  37674  poimirlem27  37676  poimirlem31  37680  ovoliunnfl  37691  itg2addnclem  37700  sstotbnd3  37805  heibor1lem  37838  heibor1  37839  rngmgmbs4  37960  exmid2  38128  redundss3  38651  redundpim3  38653  dalem53  39749  dalem54  39750  linepsubN  39776  pmapsub  39792  elpaddri  39826  pclfinN  39924  pclcmpatN  39925  cdlemg33c0  40726  dihatexv2  41363  eldioph4i  42810  acongtr  42977  pwfi2f1o  43095  aaitgo  43161  tfsconcat0b  43345  frege54cor0a  43862  clsf2  44125  ismnushort  44300  dvsconst  44329  mptssid  45245  xlimxrre  45840  icccncfext  45896  dvmptfprod  45954  stoweidlem17  46026  elaa2  46243  dmfcoafv  47184  elfzelfzlble  47330  prprelprb  47511  fmtnoprmfac1  47559  fmtnoprmfac2  47561  flsqrt  47587  lighneallem3  47601  proththd  47608  evenprm2  47708  gbogbow  47750  clnbgrel  47822  clnbgredg  47833  uhgrimisgrgric  47924  isubgr3stgrlem1  47958  isubgr3stgr  47967  gpg3nbgrvtx0  48058  gpgvtxdg3  48064  2zrngnmrid  48211  rhmsubcALTVlem3  48238  linccl  48370  lincvalpr  48374  lincdifsn  48380  lincext1  48410  lindslinindsimp1  48413  ldepspr  48429  lincresunit3lem1  48435  logblt1b  48524  dignnld  48563  dig1  48568  dignn0flhalflem1  48575  itcovalsucov  48628  line  48692  rrxline  48694  rrxsphere  48708  itschlc0xyqsol1  48726  itsclc0xyqsolr  48729  lubeldm2  48910  glbeldm2  48911  amgmwlem  49646