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

Theorem anim2i 592
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 589 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  sylanl2  684  sylanr2  686  andi  929  19.41v  1917  sbimi  1943  exdistrf  2364  equs45f  2378  moaneu  2562  darii  2594  festino  2600  baroco  2601  r19.27v  3099  rspc2ev  3355  reu3  3429  difrab  3934  copsexg  4985  imainss  5583  trssord  5778  ordnbtwn  5854  ordnbtwnOLD  5855  fof  6153  f1ocnv  6187  fv3  6244  fvelimab  6292  dff2  6411  dffo5  6416  foco2  6419  fnsnb  6473  tpres  6507  f13dfv  6570  dff1o6  6571  oprabid  6717  ssoprab2i  6791  ndmovass  6864  ndmovdistr  6865  elovmpt3rab1  6935  tfi  7095  find  7133  releldm2  7262  bropopvvv  7300  bropfvvvvlem  7301  ressuppssdif  7361  supp0cosupp0  7379  imacosupp  7380  dfrecs3  7514  omlimcl  7703  odi  7704  ixpf  7972  infcntss  8275  funsnfsupp  8340  hartogs  8490  card2on  8500  zfreg  8541  epfrs  8645  acni3  8908  dfac2  8991  cflm  9110  axdc2lem  9308  ac6s  9344  ondomon  9423  axregndlem1  9462  axregnd  9464  eltsk2g  9611  grothpw  9686  grothpwex  9687  grothomex  9689  ltexprlem1  9896  ltexprlem4  9899  recexsrlem  9962  lediv2a  10955  lbreu  11011  elfzp12  12457  dfceil2  12680  focdmex  13179  hashf1rn  13181  hashdifpr  13241  hashge2el2dif  13300  ccatsymb  13400  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12  13537  repswsymball  13572  cshwidxmod  13595  repswcshw  13604  cshimadifsn  13621  cshimadifsn0  13622  wwlktovfo  13747  relexpsucnnl  13816  cau3lem  14138  rlimres  14333  dvdsnegb  15046  dvds2add  15062  dvds2sub  15063  ndvdssub  15180  gcd2n0cl  15278  lcmfun  15405  divgcdcoprmex  15427  cncongr1  15428  powm2modprm  15555  cshwshashlem2  15850  isfunc  16571  drsdirfi  16985  gimcnv  17756  gaid  17778  symg2bas  17864  gsummptnn0fz  18428  lmhmlem  19077  lmimcnv  19115  abvn0b  19350  prmirredlem  19889  psgndiflemB  19994  matbas2  20275  matsubgcell  20288  tposmap  20311  mat1dim0  20327  mat1dimid  20328  mat1dimscm  20329  mat1dimmul  20330  dmatmul  20351  dmatcrng  20356  scmatcrng  20375  scmatf1  20385  1marepvsma1  20437  maducoeval2  20494  smadiadetlem3lem0  20519  slesolinv  20534  cramerimplem1  20537  cramerimplem2  20538  1pmatscmul  20555  cpmatacl  20569  cpmatmcllem  20571  cpmatmcl  20572  mat2pmatf1  20582  mat2pmatghm  20583  mat2pmatmul  20584  mat2pmatlin  20588  mat2pmatscmxcl  20593  m2cpmmhm  20598  m2pmfzgsumcl  20601  m2cpmrngiso  20611  decpmatmul  20625  pmatcollpw2lem  20630  monmatcollpw  20632  pmatcollpwfi  20635  pmatcollpw3fi1lem2  20640  pmatcollpwscmatlem1  20642  pmatcollpwscmatlem2  20643  pmatcollpwscmat  20644  pm2mpghm  20669  pm2mpmhmlem2  20672  pm2mp  20678  chmatcl  20681  chmatval  20682  chmaidscmat  20701  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulcl  20710  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmidgsumm2pm  20722  cpmidpmatlem2  20724  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmidgsum2  20732  cpmadumatpolylem2  20735  cayhamlem2  20737  chcoeffeqlem  20738  cayleyhamilton0  20742  cayleyhamiltonALT  20744  toprntopon  20777  toponcom  20780  neitr  21032  cnprest  21141  nrmsep2  21208  bwth  21261  2ndcsep  21310  isref  21360  reghaus  21676  isfil2  21707  alexsubALTlem3  21900  cnextcn  21918  lpbl  22355  cmodscmulexp  22968  iscau4  23123  caussi  23141  cmetcusp  23196  ovolicc2lem3  23333  limcresi  23694  elply2  23997  elqaa  24122  aannenlem1  24128  aannenlem2  24129  relogbreexp  24558  cxplogb  24569  bpos1lem  25052  axcont  25901  usgrexmplef  26196  subupgr  26224  cplgr3v  26387  cusgrfilem2  26408  usgredgsscusgredg  26411  rusgrprop0  26519  uspgr2wlkeqi  26600  spthonpthon  26703  usgr2wlkspthlem1  26709  usgr2wlkspthlem2  26710  usgr2trlncl  26712  clwlkcompim  26732  clwlkl1loop  26734  wlkwwlkinj  26850  wwlksnred  26855  wwlksnextbi  26857  wwlksnfi  26869  clwwlknclwwlkdifsOLD  26947  clwlksf1clwwlklem0  27051  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  clwwlknun  27087  clwwlknunOLD  27091  1pthon2v  27131  frcond1  27246  frcond4  27250  frgrnbnb  27273  clwwlkccat  27332  numclwwlkovh  27353  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2  27361  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwwlk2OLD  27368  frgrregord013  27382  isgrpo  27479  vcz  27558  hvsub4  28022  hvaddsub4  28063  5oalem2  28642  5oalem5  28645  5oalem6  28646  3oalem2  28650  homcl  28733  hoadddi  28790  stle0i  29226  spansncv2  29280  mdsymlem1  29390  cdj3lem1  29421  disjin  29525  disjin2  29526  f1ocnt  29687  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  pmtrprfv2  29976  crefdf  30043  sxbrsigalem0  30461  dya2icoseg2  30468  eulerpartlemgvv  30566  ballotlemirc  30721  bnj168  30924  bnj546  31092  bnj594  31108  bnj1097  31175  bnj1110  31176  bnj1174  31197  bnj1176  31199  fv1stcnv  31804  noetalem5  31992  colineardim1  32293  idinside  32316  finminlem  32437  ivthALT  32455  lukshef-ax2  32539  bj-19.41al  32762  bj-equs45fv  32877  bj-rest10b  33167  bj-ccinftydisj  33230  mptsnunlem  33315  topdifinffinlem  33325  relowlssretop  33341  elxp8  33349  matunitlindflem1  33535  poimirlem22  33561  poimirlem25  33564  poimirlem27  33566  poimirlem31  33570  ovoliunnfl  33581  itg2addnclem  33591  indexa  33658  sstotbnd3  33705  heibor1lem  33738  heibor1  33739  rngmgmbs4  33860  exmid2  34031  dalem53  35329  dalem54  35330  linepsubN  35356  pmapsub  35372  elpaddri  35406  pclfinN  35504  pclcmpatN  35505  cdlemg33c0  36307  dihatexv2  36945  eldioph4i  37693  acongtr  37862  pwfi2f1o  37983  aaitgo  38049  frege54cor0a  38474  clsf2  38741  dvsconst  38846  xlimxrre  40375  icccncfext  40418  stoweidlem17  40552  elaa2  40769  dmfcoafv  41576  elfzelfzlble  41656  pfxn0  41719  swrdpfx  41739  pfxpfx  41740  pfxccatin12lem2  41749  pfxccatin12  41750  repswpfx  41761  pfxco  41763  fmtnoprmfac1  41802  fmtnoprmfac2  41804  flsqrt  41833  lighneallem3  41849  proththd  41856  evenprm2  41948  gbogbow  41969  uspgrsprfo  42081  c0mgm  42234  c0rhm  42237  rhmisrnghm  42245  lidlmmgm  42250  2zrngnmrid  42275  rhmsubcrngclem1  42352  srhmsubclem1  42398  rhmsubcALTVlem3  42431  linccl  42528  lincvalpr  42532  lincdifsn  42538  lincext1  42568  lindslinindsimp1  42571  ldepspr  42587  lincresunit3lem1  42593  logblt1b  42683  dignnld  42722  dig1  42727  dignn0flhalflem1  42734  amgmwlem  42876
  Copyright terms: Public domain W3C validator