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

Theorem anim2i 569
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 566 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sylanl2  651  sylanr2  653  andi  867  stoic1a  1605  sbimi  1745  exdistrf  2075  equs45f  2091  moaneu  2354  2eu1OLD  2377  darii  2398  festino  2404  baroco  2405  r19.27v  2990  rspc2ev  3221  reu3  3289  difrab  3771  copsexg  4737  trssord  4900  ordnbtwn  4973  imainss  5426  fof  5800  f1ocnv  5833  fv3  5884  fvelimab  5929  dff2  6043  dffo5  6048  fnsnb  6090  f13dfv  6180  dff1o6  6181  oprabid  6323  ssoprab2i  6391  ndmovass  6463  ndmovdistr  6464  elovmpt3rab1  6536  tfi  6688  find  6725  releldm2  6850  bropopvvv  6880  ressuppssdif  6940  supp0cosupp0  6958  imacosupp  6959  omlimcl  7246  odi  7247  ixpf  7511  infcntss  7814  funsnfsupp  7873  hartogs  7990  card2on  8001  epfrs  8183  acni3  8449  dfac2  8532  cflm  8651  axdc2lem  8849  ac6s  8885  ondomon  8959  axregndlem1  9000  axregnd  9002  axregndOLD  9003  eltsk2g  9150  grothpw  9225  grothpwex  9226  grothomex  9228  ltexprlem1  9435  ltexprlem4  9438  recexsrlem  9501  lediv2a  10464  lbreu  10518  elfzp12  11786  dfceil2  11968  hashge2el2dif  12521  ccatsymb  12600  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12  12716  repswsymball  12751  cshwidxmod  12774  repswcshw  12780  wwlktovfo  12896  cau3lem  13187  rlimres  13381  dvdsnegb  14001  dvds2add  14015  dvds2sub  14016  ndvdssub  14065  powm2modprm  14328  cshwshashlem2  14581  isfunc  15233  drsdirfi  15567  gimcnv  16315  gaid  16337  symg2bas  16423  gsummptnn0fz  17014  lmhmlem  17675  lmimcnv  17713  abvn0b  17951  prmirredlem  18523  prmirredlemOLD  18526  psgndiflemB  18636  matbas2  18923  matsubgcell  18936  tposmap  18959  mat1dim0  18975  mat1dimid  18976  mat1dimscm  18977  mat1dimmul  18978  dmatmul  18999  dmatcrng  19004  scmatcrng  19023  scmatf1  19033  1marepvsma1  19085  maducoeval2  19142  smadiadetlem3lem0  19167  slesolinv  19182  cramerimplem1  19185  cramerimplem2  19186  1pmatscmul  19203  cpmatacl  19217  cpmatmcllem  19219  cpmatmcl  19220  mat2pmatf1  19230  mat2pmatghm  19231  mat2pmatmul  19232  mat2pmatlin  19236  mat2pmatscmxcl  19241  m2cpmmhm  19246  m2pmfzgsumcl  19249  m2cpmrngiso  19259  decpmatmul  19273  pmatcollpw2lem  19278  monmatcollpw  19280  pmatcollpwfi  19283  pmatcollpw3fi1lem2  19288  pmatcollpwscmatlem1  19290  pmatcollpwscmatlem2  19291  pmatcollpwscmat  19292  pm2mpghm  19317  pm2mpmhmlem2  19320  pm2mp  19326  chmatcl  19329  chmatval  19330  chmaidscmat  19349  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmulcl  19358  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cayhamlem1  19367  cpmidgsumm2pm  19370  cpmidpmatlem2  19372  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  cpmadugsumfi  19378  cpmidgsum2  19380  cpmadumatpolylem2  19383  cayhamlem2  19385  chcoeffeqlem  19386  cayleyhamilton0  19390  cayleyhamiltonALT  19392  toponcom  19431  neitr  19681  cnprest  19790  nrmsep2  19857  bwth  19910  2ndcsep  19960  isref  20010  reghaus  20326  isfil2  20357  alexsubALTlem3  20549  cnextcn  20567  lpbl  21006  iscau4  21718  caussi  21736  cmetcuspOLD  21793  cmetcusp  21794  ovolicc2lem3  21930  limcresi  22289  elply2  22593  elqaa  22718  aannenlem1  22724  aannenlem2  22725  bpos1lem  23557  axcont  24279  uhgrares  24308  usgraop  24350  usgrares  24369  usgraexmpl  24401  cusgra3v  24464  cusgrafilem2  24480  redwlk  24608  wlkdvspthlem  24609  cyclispthon  24633  usgrcyclnl1  24640  3v3e3cycl1  24644  wwlknimp  24687  wlkiswwlkfun  24717  wlkiswwlkinj  24718  wwlknred  24723  wwlknextbi  24725  wwlknfi  24738  clwwlknprop  24772  wwlkext2clwwlk  24803  clwwnisshclwwn  24809  eleclclwwlknlem1  24817  clwlkfoclwwlk  24845  2wlkonotv  24877  clwlknclwlkdifs  24960  eupatrl  24968  frgraunss  24995  frgranbnb  25020  frgrawopreg  25049  frg2woteq  25060  numclwlk3lem3  25073  numclwwlkffin  25082  numclwwlkovf2ex  25086  numclwwlk1  25098  numclwwlkqhash  25100  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwwlk5  25112  numclwwlk7  25114  frgraregord013  25118  isgrpo  25198  gxsub  25278  rngmgmbs4  25419  vcz  25463  sspival  25651  hvsub4  25954  hvaddsub4  25995  5oalem2  26573  5oalem5  26576  5oalem6  26577  3oalem2  26581  homcl  26665  hoadddi  26722  stle0i  27158  spansncv2  27212  mdsymlem1  27322  cdj3lem1  27353  disjin  27446  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  crefdf  27851  sxbrsigalem0  28242  dya2icoseg2  28249  eulerpartlemgvv  28315  ballotlemirc  28470  colineardim1  29711  idinside  29734  lukshef-ax2  29880  ovoliunnfl  30056  itg2addnclem  30066  finminlem  30136  ivthALT  30153  indexa  30224  sstotbnd3  30272  heibor1lem  30305  heibor1  30306  exmid2  30499  eldioph4i  30746  acongtr  30916  aaitgo  31111  dvsconst  31235  icccncfext  31690  stoweidlem17  31799  dmfcoafv  32260  elfzelfzlble  32337  tpres  32554  c0mgm  32715  c0rhm  32718  rhmisrnghm  32726  lidlmmgm  32731  2zrngnmrid  32756  rhmsubcrngclem1  32835  srhmsubclem1  32881  srhmsubcOLDlem1  32900  rhmsubcOLDlem3  32915  linccl  33015  lincvalpr  33019  lincdifsn  33025  lincext1  33055  lindslinindsimp1  33058  ldepspr  33074  lincresunit3lem1  33080  bnj145OLD  33782  bnj168  33785  bnj546  33954  bnj594  33970  bnj1097  34037  bnj1110  34038  bnj1174  34059  bnj1176  34061  bj-equs45fv  34331  bj-ccinftydisj  34616  dalem53  35449  dalem54  35450  linepsubN  35476  pmapsub  35492  elpaddri  35526  pclfinN  35624  pclcmpatN  35625  cdlemg33c0  36428  dihatexv2  37066  frege54cor0a  37890
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 185  df-an 371
  Copyright terms: Public domain W3C validator