MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim2i Structured version   Visualization version   GIF version

Theorem anim2i 605
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
StepHypRef Expression
1 id 22 . 2 (𝜒𝜒)
2 anim1i.1 . 2 (𝜑𝜓)
31, 2anim12i 602 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  sylanl2  663  sylanr2  665  andi  1021  19.41v  2040  sbimi  2066  exdistrf  2495  equs45f  2508  moaneu  2697  dariiALT  2730  festinoALT  2741  barocoALT  2743  r19.27v  3258  rspc2ev  3517  reu3  3594  difrab  4102  opthprneg  4587  copsexg  5145  imainss  5759  trssord  5953  ordnbtwn  6029  ordnbtwnOLD  6030  fof  6331  f1ocnv  6365  fv3  6426  fvelimab  6474  dff2  6593  dffo5  6598  foco2  6601  fnsnb  6657  tpres  6691  f13dfv  6754  dff1o6  6755  oprabid  6905  ssoprab2i  6979  ndmovass  7052  ndmovdistr  7053  elovmpt3rab1  7123  tfi  7283  find  7321  releldm2  7450  bropopvvv  7489  bropfvvvvlem  7490  ressuppssdif  7550  supp0cosupp0  7569  imacosupp  7570  dfrecs3  7705  omlimcl  7895  odi  7896  ixpf  8167  snmapen  8273  infcntss  8473  funsnfsupp  8538  hartogs  8688  card2on  8698  zfreg  8739  epfrs  8854  acni3  9153  dfac2b  9236  dfac2OLD  9238  cflm  9357  axdc2lem  9555  ac6s  9591  ondomon  9670  axregndlem1  9709  axregnd  9711  eltsk2g  9858  grothpw  9933  grothpwex  9934  grothomex  9936  ltexprlem1  10143  ltexprlem4  10146  recexsrlem  10209  lediv2a  11202  lbreu  11258  elfzp12  12642  dfceil2  12864  focdmex  13359  hashf1rn  13361  hashdifpr  13420  hashge2el2dif  13479  ccatsymb  13579  swrdccatin2  13711  swrdccatin12lem2  13713  swrdccatin12  13715  repswsymball  13750  cshwidxmod  13773  repswcshw  13782  cshimadifsn  13799  cshimadifsn0  13800  wwlktovfo  13926  relexpsucnnl  13995  cau3lem  14317  rlimres  14512  dvdsnegb  15222  dvds2add  15238  dvds2sub  15239  ndvdssub  15352  gcd2n0cl  15450  lcmfun  15577  divgcdcoprmex  15598  cncongr1  15599  powm2modprm  15725  cshwshashlem2  16015  isfunc  16728  drsdirfi  17143  gimcnv  17911  gaid  17933  symg2bas  18019  gsummptnn0fz  18583  gsummptnn0fzOLD  18584  lmhmlem  19236  lmimcnv  19274  abvn0b  19511  prmirredlem  20049  psgndiflemB  20154  matbas2  20437  matsubgcell  20450  tposmap  20474  mat1dim0  20490  mat1dimid  20491  mat1dimscm  20492  mat1dimmul  20493  dmatmul  20514  dmatcrng  20519  scmatcrng  20538  scmatf1  20548  1marepvsma1  20600  maducoeval2  20657  smadiadetlem3lem0  20683  slesolinv  20698  cramerimplem1  20701  cramerimplem1OLD  20702  cramerimplem2  20703  1pmatscmul  20720  cpmatacl  20734  cpmatmcllem  20736  cpmatmcl  20737  mat2pmatf1  20747  mat2pmatghm  20748  mat2pmatmul  20749  mat2pmatlin  20753  mat2pmatscmxcl  20758  m2cpmmhm  20763  m2pmfzgsumcl  20766  m2cpmrngiso  20776  decpmatmul  20790  pmatcollpw2lem  20795  monmatcollpw  20797  pmatcollpwfi  20800  pmatcollpw3fi1lem2  20805  pmatcollpwscmatlem1  20807  pmatcollpwscmatlem2  20808  pmatcollpwscmat  20809  pm2mpghm  20834  pm2mpmhmlem2  20837  pm2mp  20843  chmatcl  20846  chmatval  20847  chmaidscmat  20866  chfacfisf  20872  chfacfisfcpmat  20873  chfacfscmulcl  20875  chfacfscmul0  20876  chfacfscmulgsum  20878  chfacfpmmul0  20880  chfacfpmmulgsum  20882  chfacfpmmulgsum2  20883  cayhamlem1  20884  cpmidgsumm2pm  20887  cpmidpmatlem2  20889  cpmadugsumlemB  20892  cpmadugsumlemC  20893  cpmadugsumlemF  20894  cpmadugsumfi  20895  cpmidgsum2  20897  cpmadumatpolylem2  20900  cayhamlem2  20902  chcoeffeqlem  20903  cayleyhamilton0  20907  cayleyhamiltonALT  20909  toprntopon  20943  toponcom  20946  neitr  21198  cnprest  21307  nrmsep2  21374  bwth  21427  2ndcsep  21476  isref  21526  reghaus  21842  isfil2  21873  alexsubALTlem3  22066  cnextcn  22084  lpbl  22521  cmodscmulexp  23134  iscau4  23289  caussi  23307  cmetcusp  23362  ovolicc2lem3  23500  limcresi  23863  elply2  24166  elqaa  24291  aannenlem1  24297  aannenlem2  24298  relogbreexp  24727  cxplogb  24738  bpos1lem  25221  axcont  26070  usgrexmplef  26367  subupgr  26395  cplgr3v  26559  cusgrfilem2  26580  usgredgsscusgredg  26583  rusgrprop0  26691  uspgr2wlkeqi  26772  spthonpthon  26875  usgr2wlkspthlem1  26881  usgr2wlkspthlem2  26882  usgr2trlncl  26884  clwlkcompim  26904  clwlkl1loop  26907  wlkwwlkinjOLD  27024  wwlksnred  27029  wwlksnextbi  27031  wwlksnfi  27043  clwwlknclwwlkdifsOLD  27122  clwwlkccat  27133  clwlksf1clwwlklem0OLD  27238  clwwlknonwwlknonb  27274  clwwlknonwwlknonbOLD  27275  clwwlknun  27281  clwwlknunOLD  27286  1pthon2v  27326  frcond1  27441  frcond4  27445  frgrnbnb  27468  clwlknon2num  27548  numclwlk1lem1  27549  numclwlk1lem2  27550  numclwwlkovh  27553  numclwwlk2lem1  27556  numclwlk2lem2f  27557  numclwwlk2  27561  numclwwlk2lem1OLD  27563  numclwlk2lem2fOLD  27564  numclwwlk2OLD  27568  frgrregord013  27583  isgrpo  27680  vcz  27758  hvsub4  28222  hvaddsub4  28263  5oalem2  28842  5oalem5  28845  5oalem6  28846  3oalem2  28850  homcl  28933  hoadddi  28990  stle0i  29426  spansncv2  29480  mdsymlem1  29590  cdj3lem1  29621  disjin  29724  disjin2  29725  f1ocnt  29886  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  pmtrprfv2  30173  crefdf  30240  sxbrsigalem0  30658  dya2icoseg2  30665  eulerpartlemgvv  30763  ballotlemirc  30918  bnj168  31121  bnj546  31289  bnj594  31305  bnj1097  31372  bnj1110  31373  bnj1174  31394  bnj1176  31396  fv1stcnv  32000  noetalem5  32188  colineardim1  32489  idinside  32512  finminlem  32633  ivthALT  32651  lukshef-ax2  32731  bj-19.41al  32952  bj-equs45fv  33066  bj-rest10b  33353  bj-ccinftydisj  33417  mptsnunlem  33502  topdifinffinlem  33511  relowlssretop  33527  elxp8  33535  matunitlindflem1  33718  poimirlem22  33744  poimirlem25  33747  poimirlem27  33749  poimirlem31  33753  ovoliunnfl  33764  itg2addnclem  33773  indexa  33840  sstotbnd3  33886  heibor1lem  33919  heibor1  33920  rngmgmbs4  34041  exmid2  34212  dalem53  35505  dalem54  35506  linepsubN  35532  pmapsub  35548  elpaddri  35582  pclfinN  35680  pclcmpatN  35681  cdlemg33c0  36483  dihatexv2  37120  eldioph4i  37878  acongtr  38046  pwfi2f1o  38167  aaitgo  38233  frege54cor0a  38657  clsf2  38924  dvsconst  39029  xlimxrre  40537  icccncfext  40580  stoweidlem17  40713  elaa2  40930  fundmdfat  41718  dmfcoafv  41764  elfzelfzlble  41906  pfxn0  41969  swrdpfx  41989  pfxpfx  41990  pfxccatin12lem2  41999  pfxccatin12  42000  repswpfx  42011  pfxco  42013  fmtnoprmfac1  42052  fmtnoprmfac2  42054  flsqrt  42083  lighneallem3  42099  proththd  42106  evenprm2  42198  gbogbow  42219  uspgrsprfo  42324  c0mgm  42477  c0rhm  42480  rhmisrnghm  42488  lidlmmgm  42493  2zrngnmrid  42518  rhmsubcrngclem1  42595  srhmsubclem1  42641  rhmsubcALTVlem3  42674  linccl  42771  lincvalpr  42775  lincdifsn  42781  lincext1  42811  lindslinindsimp1  42814  ldepspr  42830  lincresunit3lem1  42836  logblt1b  42926  dignnld  42965  dig1  42970  dignn0flhalflem1  42977  amgmwlem  43119
  Copyright terms: Public domain W3C validator