Theorem anim2i 623

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 619	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylanr2  689  andi  1015  19.41v  1956  exdistrf  2455  equs45f  2467  moaneu  2627  dariiALT  2670  festinoALT  2679  barocoALT  2681  r19.27v  3169  rspc2ev  3580  reu3  3675  difrab  4253  opthprneg  4803  copsexgwOLD  5438  copsexg  5439  imainss  6112  trssord  6334  ordnbtwn  6412  fof  6746  fv3  6852  fvelimab  6906  dff2  7047  dffo5  7052  foco2  7057  fnsnbOLD  7117  tpres  7152  f13dfv  7225  dff1o6  7226  oprabidw  7394  oprabid  7395  ssoprab2i  7474  ndmovass  7551  ndmovdistr  7552  elovmpt3rab1  7623  tfi  7800  find  7842  releldm2  7992  bropopvvv  8036  bropfvvvvlem  8037  ressuppssdif  8132  omlimcl  8510  odi  8511  ixpf  8865  dif1en  9093  domtrfil  9123  funsnfsupp  9302  hartogs  9456  card2on  9466  zfreg  9508  epfrs  9650  acni3  9967  dfac2b  10051  cflm  10170  axdc2lem  10368  ac6s  10404  ondomon  10483  axregndlem1  10523  axregnd  10525  eltsk2g  10672  grothpw  10747  grothpwex  10748  grothomex  10750  ltexprlem1  10957  ltexprlem4  10960  recexsrlem  11024  elfzp12  13555  hashf1rn  14312  hashdifpr  14375  hashgt23el  14384  hashge2el2dif  14440  ccatsymb  14543  swrdnd0  14618  swrdpfx  14667  pfxpfx  14668  pfxccatin12  14693  cshwidxmod  14763  repswcshw  14772  cshimadifsn  14789  cshimadifsn0  14790  pfxco  14798  wwlktovfo  14918  relexpsucnnl  14990  cau3lem  15315  rlimres  15518  dvdsnegb  16240  dvds2add  16257  dvds2sub  16258  nn0onn  16347  gcd2n0cl  16476  lcmfun  16612  divgcdcoprmex  16633  cncongr1  16634  isfunc  17829  drsdirfi  18269  chnrev  18591  sgrpidmnd  18705  smndex1iidm  18867  gaid  19272  symg2bas  19366  qusecsub  19808  gsumle  20118  c0mgm  20437  rhmisrnghm  20458  c0rhm  20513  rhmsubcrngclem1  20645  srhmsubclem1  20656  abvn0b  20815  lmhmlem  21026  prmirredlem  21454  psgndiflemB  21582  ismhp  22135  matsubgcell  22424  tposmap  22447  mat1dim0  22463  mat1dimid  22464  mat1dimscm  22465  mat1dimmul  22466  dmatmul  22487  dmatcrng  22492  scmatcrng  22511  scmatf1  22521  1marepvsma1  22573  maducoeval2  22630  smadiadetlem3lem0  22655  slesolinv  22670  cramerimplem1  22673  cramerimplem2  22674  1pmatscmul  22692  cpmatacl  22706  cpmatmcllem  22708  cpmatmcl  22709  mat2pmatf1  22719  mat2pmatghm  22720  mat2pmatmul  22721  mat2pmatlin  22725  mat2pmatscmxcl  22730  m2cpmmhm  22735  m2pmfzgsumcl  22738  decpmatmul  22762  pmatcollpw2lem  22767  monmatcollpw  22769  pmatcollpwfi  22772  pmatcollpw3fi1lem2  22777  pmatcollpwscmatlem1  22779  pmatcollpwscmatlem2  22780  pmatcollpwscmat  22781  pm2mpghm  22806  pm2mpmhmlem2  22809  pm2mp  22815  chmatcl  22818  chmatval  22819  chmaidscmat  22838  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulcl  22847  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmidgsumm2pm  22859  cpmidpmatlem2  22861  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cpmadugsumfi  22867  cpmidgsum2  22869  cpmadumatpolylem2  22872  cayhamlem2  22874  chcoeffeqlem  22875  cayleyhamilton0  22879  cayleyhamiltonALT  22881  toponcom  22918  neitr  23170  cnprest  23279  nrmsep2  23346  bwth  23400  2ndcsep  23449  isref  23499  reghaus  23815  isfil2  23846  alexsubALTlem3  24039  cnextcn  24057  lpbl  24493  cmodscmulexp  25114  iscau4  25271  caussi  25289  cmetcusp  25346  ovolicc2lem3  25511  limcresi  25877  elply2  26186  elqaa  26313  aannenlem1  26319  aannenlem2  26320  relogbreexp  26764  cxplogb  26775  bpos1lem  27270  noetalem2  27731  tgjustc1  28568  tgjustc2  28569  axcont  29070  usgrexmplef  29353  subupgr  29381  cplgr3v  29529  cusgrfilem2  29550  usgredgsscusgredg  29553  rusgrprop0  29661  uspgr2wlkeqi  29741  trlontrl  29802  spthonpthon  29844  usgr2wlkspthlem1  29850  usgr2wlkspthlem2  29851  clwlkcompim  29873  clwlkl1loop  29876  wwlksnred  29985  clwwlknonwwlknonb  30201  clwwlknun  30207  1pthon2v  30248  frcond1  30361  frcond4  30365  frgrnbnb  30388  clwlknon2num  30463  numclwlk1lem1  30464  numclwlk1lem2  30465  numclwwlkovh  30468  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwwlk2  30476  isgrpo  30593  vcz  30671  hvsub4  31133  hvaddsub4  31174  5oalem2  31751  5oalem5  31754  5oalem6  31755  3oalem2  31759  homcl  31842  hoadddi  31899  stle0i  32335  spansncv2  32389  mdsymlem1  32499  cdj3lem1  32530  f1ocnt  32899  gsumvsca1  33314  gsumvsca2  33315  crefdf  34039  sxbrsigalem0  34462  dya2icoseg2  34469  eulerpartlemgvv  34567  ballotlemirc  34723  bnj168  34920  bnj546  35085  bnj594  35101  bnj1097  35170  bnj1110  35171  bnj1174  35192  bnj1176  35194  axprALT2  35297  cusgredgex2  35358  acycgrislfgr  35387  umgracycusgr  35389  cusgracyclt3v  35391  satfv1  35598  satf0suclem  35610  fmlasuc0  35619  fmlafvel  35620  satffunlem2lem1  35639  satfun  35646  fv1stcnv  36012  colineardim1  36296  idinside  36319  finminlem  36553  ivthALT  36570  lukshef-ax2  36650  regsfromregtco  36773  bj-19.41al  37006  bj-equs45fv  37171  bj-elabd2ALT  37285  bj-rest10b  37454  copsex2b  37507  bj-elid6  37537  bj-ccinftydisj  37580  mptsnunlem  37707  topdifinffinlem  37716  relowlssretop  37732  elxp8  37740  fvineqsnf1  37779  pibt1  37785  matunitlindflem1  37990  poimirlem22  38016  poimirlem25  38019  poimirlem27  38021  poimirlem31  38025  ovoliunnfl  38036  itg2addnclem  38045  sstotbnd3  38150  heibor1lem  38183  heibor1  38184  rngmgmbs4  38305  exmid2  38473  redundss3  39086  redundpim3  39088  dalem53  40224  dalem54  40225  linepsubN  40251  pmapsub  40267  elpaddri  40301  pclfinN  40399  pclcmpatN  40400  cdlemg33c0  41201  dihatexv2  41838  eldioph4i  43264  acongtr  43430  pwfi2f1o  43548  aaitgo  43614  tfsconcat0b  43798  frege54cor0a  44314  clsf2  44577  ismnushort  44752  dvsconst  44781  mptssid  45692  xlimxrre  46281  icccncfext  46337  dvmptfprod  46395  stoweidlem17  46467  elaa2  46684  dmfcoafv  47645  elfzelfzlble  47791  prprelprb  47999  fmtnoprmfac1  48050  fmtnoprmfac2  48052  flsqrt  48078  lighneallem3  48092  proththd  48099  evenprm2  48212  gbogbow  48254  clnbgrel  48326  clnbgredg  48338  uhgrimisgrgric  48429  isubgr3stgrlem1  48464  isubgr3stgr  48473  gpg3nbgrvtx0  48574  gpgvtxdg3  48580  2zrngnmrid  48754  rhmsubcALTVlem3  48781  linccl  48912  lincvalpr  48916  lincdifsn  48922  lincext1  48952  lindslinindsimp1  48955  ldepspr  48971  lincresunit3lem1  48977  logblt1b  49062  dignnld  49101  dig1  49106  dignn0flhalflem1  49113  itcovalsucov  49166  line  49230  rrxline  49232  rrxsphere  49246  itschlc0xyqsol1  49264  itsclc0xyqsolr  49267  lubeldm2  49453  glbeldm2  49454  isinito4a  50045  amgmwlem  50299