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

Theorem anim2i 618
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 614 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  sylanr2  681  andi  1003  19.41v  1943  exdistrf  2462  equs45f  2475  sbimiOLD  2509  sbimiALT  2571  moaneu  2702  dariiALT  2747  festinoALT  2756  barocoALT  2758  r19.27v  3182  r19.27vOLD  3183  rspc2ev  3633  reu3  3716  difrab  4275  opthprneg  4787  copsexgw  5372  copsexg  5373  imainss  6004  trssord  6201  ordnbtwn  6274  fof  6583  fv3  6681  fvelimab  6730  dff2  6858  dffo5  6863  foco2  6866  fnsnb  6921  tpres  6956  f13dfv  7023  dff1o6  7024  oprabidw  7179  oprabid  7180  ssoprab2i  7255  ndmovass  7328  ndmovdistr  7329  elovmpt3rab1  7397  tfi  7560  find  7599  releldm2  7734  bropopvvv  7777  bropfvvvvlem  7778  ressuppssdif  7843  supp0cosupp0OLD  7865  imacosuppOLD  7867  omlimcl  8196  odi  8197  ixpf  8476  funsnfsupp  8849  hartogs  9000  card2on  9010  zfreg  9051  epfrs  9165  acni3  9465  dfac2b  9548  cflm  9664  axdc2lem  9862  ac6s  9898  ondomon  9977  axregndlem1  10016  axregnd  10018  eltsk2g  10165  grothpw  10240  grothpwex  10241  grothomex  10243  ltexprlem1  10450  ltexprlem4  10453  recexsrlem  10517  elfzp12  12978  focdmex  13703  hashf1rn  13705  hashdifpr  13768  hashgt23el  13777  hashge2el2dif  13830  ccatsymb  13928  swrdnd0  14011  swrdpfx  14061  pfxpfx  14062  pfxccatin12  14087  cshwidxmod  14157  repswcshw  14166  cshimadifsn  14183  cshimadifsn0  14184  pfxco  14192  wwlktovfo  14314  relexpsucnnl  14383  cau3lem  14706  rlimres  14907  dvdsnegb  15619  dvds2add  15635  dvds2sub  15636  nn0onn  15723  gcd2n0cl  15850  lcmfun  15981  divgcdcoprmex  16002  cncongr1  16003  isfunc  17126  drsdirfi  17540  sgrpidmnd  17908  smndex1iidm  18058  gaid  18421  symg2bas  18513  lmhmlem  19793  abvn0b  20067  prmirredlem  20632  psgndiflemB  20736  matsubgcell  21035  tposmap  21058  mat1dim0  21074  mat1dimid  21075  mat1dimscm  21076  mat1dimmul  21077  dmatmul  21098  dmatcrng  21103  scmatcrng  21122  scmatf1  21132  1marepvsma1  21184  maducoeval2  21241  smadiadetlem3lem0  21266  slesolinv  21281  cramerimplem1  21284  cramerimplem2  21285  1pmatscmul  21302  cpmatacl  21316  cpmatmcllem  21318  cpmatmcl  21319  mat2pmatf1  21329  mat2pmatghm  21330  mat2pmatmul  21331  mat2pmatlin  21335  mat2pmatscmxcl  21340  m2cpmmhm  21345  m2pmfzgsumcl  21348  m2cpmrngiso  21358  decpmatmul  21372  pmatcollpw2lem  21377  monmatcollpw  21379  pmatcollpwfi  21382  pmatcollpw3fi1lem2  21387  pmatcollpwscmatlem1  21389  pmatcollpwscmatlem2  21390  pmatcollpwscmat  21391  pm2mpghm  21416  pm2mpmhmlem2  21419  pm2mp  21425  chmatcl  21428  chmatval  21429  chmaidscmat  21448  chfacfisf  21454  chfacfisfcpmat  21455  chfacfscmulcl  21457  chfacfscmul0  21458  chfacfscmulgsum  21460  chfacfpmmul0  21462  chfacfpmmulgsum  21464  chfacfpmmulgsum2  21465  cayhamlem1  21466  cpmidgsumm2pm  21469  cpmidpmatlem2  21471  cpmadugsumlemB  21474  cpmadugsumlemC  21475  cpmadugsumlemF  21476  cpmadugsumfi  21477  cpmidgsum2  21479  cpmadumatpolylem2  21482  cayhamlem2  21484  chcoeffeqlem  21485  cayleyhamilton0  21489  cayleyhamiltonALT  21491  toponcom  21528  neitr  21780  cnprest  21889  nrmsep2  21956  bwth  22010  2ndcsep  22059  isref  22109  reghaus  22425  isfil2  22456  alexsubALTlem3  22649  cnextcn  22667  lpbl  23105  cmodscmulexp  23718  iscau4  23874  caussi  23892  cmetcusp  23949  ovolicc2lem3  24112  limcresi  24475  elply2  24778  elqaa  24903  aannenlem1  24909  aannenlem2  24910  relogbreexp  25345  cxplogb  25356  bpos1lem  25850  tgjustc1  26253  tgjustc2  26254  axcont  26754  usgrexmplef  27033  subupgr  27061  cplgr3v  27209  cusgrfilem2  27230  usgredgsscusgredg  27233  rusgrprop0  27341  uspgr2wlkeqi  27421  trlontrl  27484  spthonpthon  27524  usgr2wlkspthlem1  27530  usgr2wlkspthlem2  27531  clwlkcompim  27553  clwlkl1loop  27556  wwlksnred  27662  wwlksnfiOLD  27677  clwwlknonwwlknonb  27877  clwwlknun  27883  1pthon2v  27924  frcond1  28037  frcond4  28041  frgrnbnb  28064  clwlknon2num  28139  numclwlk1lem1  28140  numclwlk1lem2  28141  numclwwlkovh  28144  numclwwlk2lem1  28147  numclwlk2lem2f  28148  numclwwlk2  28152  isgrpo  28266  vcz  28344  hvsub4  28806  hvaddsub4  28847  5oalem2  29424  5oalem5  29427  5oalem6  29428  3oalem2  29432  homcl  29515  hoadddi  29572  stle0i  30008  spansncv2  30062  mdsymlem1  30172  cdj3lem1  30203  f1ocnt  30517  gsumle  30718  gsumvsca1  30847  gsumvsca2  30848  crefdf  31100  sxbrsigalem0  31517  dya2icoseg2  31524  eulerpartlemgvv  31622  ballotlemirc  31777  bnj168  31988  bnj546  32156  bnj594  32172  bnj1097  32241  bnj1110  32242  bnj1174  32263  bnj1176  32265  cusgredgex2  32357  acycgrislfgr  32387  umgracycusgr  32389  cusgracyclt3v  32391  satfv1  32598  satf0suclem  32610  fmlasuc0  32619  fmlafvel  32620  satffunlem2lem1  32639  satfun  32646  fv1stcnv  33008  noetalem5  33209  colineardim1  33510  idinside  33533  finminlem  33654  ivthALT  33671  lukshef-ax2  33751  bj-19.41al  33980  bj-equs45fv  34121  bj-rest10b  34367  copsex2b  34419  bj-elid6  34449  bj-ccinftydisj  34482  mptsnunlem  34606  topdifinffinlem  34615  relowlssretop  34631  elxp8  34639  fvineqsnf1  34678  pibt1  34684  matunitlindflem1  34875  poimirlem22  34901  poimirlem25  34904  poimirlem27  34906  poimirlem31  34910  ovoliunnfl  34921  itg2addnclem  34930  sstotbnd3  35041  heibor1lem  35074  heibor1  35075  rngmgmbs4  35196  exmid2  35364  redundss3  35850  redundpim3  35852  dalem53  36848  dalem54  36849  linepsubN  36875  pmapsub  36891  elpaddri  36925  pclfinN  37023  pclcmpatN  37024  cdlemg33c0  37825  dihatexv2  38462  eldioph4i  39394  acongtr  39560  pwfi2f1o  39681  aaitgo  39747  frege54cor0a  40194  clsf2  40461  dvsconst  40647  mptssid  41495  xlimxrre  42096  icccncfext  42154  stoweidlem17  42287  elaa2  42504  dmfcoafv  43359  elfzelfzlble  43506  prprelprb  43664  fmtnoprmfac1  43712  fmtnoprmfac2  43714  flsqrt  43741  lighneallem3  43757  proththd  43764  evenprm2  43864  gbogbow  43906  uspgrsprfo  44008  c0mgm  44165  c0rhm  44168  rhmisrnghm  44176  lidlmmgm  44181  2zrngnmrid  44206  rhmsubcrngclem1  44283  srhmsubclem1  44329  rhmsubcALTVlem3  44362  linccl  44454  lincvalpr  44458  lincdifsn  44464  lincext1  44494  lindslinindsimp1  44497  ldepspr  44513  lincresunit3lem1  44519  logblt1b  44609  dignnld  44648  dig1  44653  dignn0flhalflem1  44660  line  44704  rrxline  44706  rrxsphere  44720  itschlc0xyqsol1  44738  itsclc0xyqsolr  44741  amgmwlem  44888
  Copyright terms: Public domain W3C validator