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

Theorem anim1i 604
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1 (𝜑𝜓)
Assertion
Ref Expression
anim1i ((𝜑𝜒) → (𝜓𝜒))

Proof of Theorem anim1i
StepHypRef Expression
1 anim1i.1 . 2 (𝜑𝜓)
2 id 22 . 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:  sylanl1  662  sylanr1  664  disamisOLD  2751  rmob  3724  eqeuel  4142  elpwdifsn  4511  preq12nebg  4585  fores  6336  ssimaex  6480  dffv2  6488  exfo  6595  frnssb  6609  fpropnf1  6744  oprabv  6929  ndmovass  7048  fun11uni  7346  fabexg  7348  f1oabexg  7351  fun11iun  7352  soxp  7520  tz7.48lem  7768  tz7.49c  7773  omass  7893  oewordri  7905  omabs  7960  sbthlem9  8313  fineqvlem  8409  pssnn  8413  domunfican  8468  fiint  8472  fsuppsssupp  8526  sup0  8607  inf1  8762  infeq5  8777  cantnfle  8811  rankuni  8969  djuunxp  9026  acndom  9153  acnnum  9154  cdainflem  9294  cfcof  9377  ac6num  9582  ac6s2  9589  brdom5  9632  brdom4  9633  genpnnp  10108  divmulasscom  10990  lediv2a  11198  supmul1  11273  infregelb  11288  nn2ge  11327  btwnz  11741  eluz2b2  11976  uz2mulcl  11981  eqreznegel  11989  xrsupexmnf  12349  xrinfmexpnf  12350  xrsupsslem  12351  xrinfmsslem  12352  supxrun  12360  ioo0  12414  elioo4g  12448  fz0fzelfz0  12665  fz0fzdiffz0  12668  2ffzeq  12680  elfzodifsumelfzo  12754  elfzom1elp1fzo  12755  zpnn0elfzo  12761  elfzom1elp1fzo1  12788  fzonfzoufzol  12791  quoremnn0  12875  zmodidfzoimp  12920  modabs  12923  modmuladd  12932  modifeq2int  12952  modaddmulmod  12957  expcl2lem  13091  hashreshashfun  13439  iswrdsymb  13529  ccatcl  13567  ccatval3  13572  ccatalpha  13586  swrdfv2  13666  swrdsbslen  13668  swrdspsleq  13669  swrd0swrd  13681  swrdccatin2  13707  swrdccatin12lem3  13710  swrdccat3  13712  swrdccat3blem  13715  swrdccatid  13717  repswccat  13752  2cshw  13779  cshweqdifid  13786  lswco  13804  repsco  13805  s4f1o  13883  ccat2s1fvwALT  13919  trclun  13974  mulre  14080  rediv  14090  imdiv  14097  resqrex  14210  caurcvg2  14627  fsumdifsnconst  14741  modfsummods  14743  tanval  15074  p1modz1  15206  negdvdsb  15217  muldvds1  15225  muldvds2  15226  dvdscmulr  15229  dvdsmulcr  15230  dvdsdivcl  15257  nn0ehalf  15311  nn0oddm1d2  15317  nnoddm1d2  15318  sumeven  15326  sumodd  15327  divalglem8  15339  divgcdnn  15451  lcmfunsnlem2lem2  15567  lcmfun  15573  coprmgcdb  15577  ncoprmgcdne1b  15578  divgcdcoprm0  15593  maxprmfct  15634  ncoprmlnprm  15649  vfermltl  15719  vfermltlALT  15720  modprm0  15723  modprmn0modprm0  15725  pcpremul  15761  pcmul  15769  dvdsprmpweqle  15803  oddprmdvds  15820  prmdvdsprmo  15959  prmgaplem4  15971  prmgaplem7  15974  cshwsidrepsw  16008  gsmsymgreqlem2  18048  symgfixfo  18056  fsfnn0gsumfsffz  18576  irredn0  18901  rim0to0  18942  lsppratlem1  19352  ixpsnbasval  19414  cply1coe0bi  19874  dvdsrzring  20035  mpt2frlmd  20323  matinvgcell  20448  mat1dimcrng  20491  dmatscmcl  20517  scmatmats  20525  scmatscm  20527  scmatmulcl  20532  scmatghm  20547  scmatmhm  20548  ma1repvcl  20584  mdet1  20615  mdet0  20620  slesolinv  20695  slesolinvbi  20696  cramerimplem1  20698  cramerimplem1OLD  20699  cramerimp  20702  cramerlem1  20703  cramer  20707  cpmatacl  20731  cpmatmcl  20734  mat2pmatghm  20745  mat2pmatmul  20746  m2pmfzgsumcl  20763  decpmatmul  20787  decpmatmulsumfsupp  20788  pmatcollpwfi  20797  pmatcollpwscmat  20806  pm2mpf1  20814  pm2mpghm  20831  pm2mpmhmlem1  20833  monmat2matmon  20839  chpdmatlem2  20854  chpdmat  20856  chfacfisf  20869  cpmadugsumlemB  20889  cpmadugsumlemC  20890  cpmadugsumlemF  20891  clscld  21062  neiptopnei  21147  2ndcdisj2  21471  comppfsc  21546  tx1stc  21664  opnfbas  21856  fbasfip  21882  alexsublem  22058  alexsubALTlem4  22064  cnextcn  22081  ngpocelbl  22718  cvsi  23139  cphipval  23251  cphsscph  23259  bcthlem5  23335  vitalilem4  23591  vitalilem5  23592  itg2mulc  23727  dvcobr  23922  dvcnvlem  23952  dvferm1  23961  dvne0  23987  mdegmullem  24051  plyeq0lem  24179  plyexmo  24281  aalioulem5  24304  aalioulem6  24305  aaliou  24306  cxple2a  24658  cxpaddlelem  24705  cxpaddle  24706  relogbcxpb  24738  bcmono  25215  lgsprme0  25277  gausslemma2dlem0e  25298  gausslemma2dlem1a  25303  gausslemma2dlem6  25310  lgsquadlem2  25319  2lgsoddprm  25354  colinearalg  26003  axcontlem3  26059  umgrislfupgrlem  26230  edgupgr  26242  usgruspgrb  26290  usgrislfuspgr  26293  edgssv2  26304  umgr2edg  26315  usgr2edg  26316  uspgredg2v  26330  usgrexmplef  26366  subupgr  26394  subusgr  26396  usgrfilem  26434  nbupgrres  26480  nb3gr2nb  26501  nbupgruvtxres  26529  cplgr3v  26558  cusgrres  26571  cusgrsizeindslem  26574  cusgrsizeinds  26575  vtxdun  26604  finrusgrfusgr  26688  cusgrrusgr  26704  wlkonprop  26781  wlkreslem  26793  trlsonprop  26831  spthdep  26857  pthsonprop  26867  spthonprop  26868  cycliscrct  26922  crctcshwlkn0lem6  26935  crctcshwlkn0lem7  26936  crctcshtrl  26943  crctcsh  26944  wlkwwlksurOLD  27024  umgr2adedgwlkonALT  27086  elwwlks2  27107  elwspths2spth  27108  rusgrnumwwlk  27116  clwwlkccatlem  27131  clwlkclwwlklem2a  27140  clwlkclwwlklem3  27143  clwwisshclwws  27157  wwlksext2clwwlkOLD  27207  wwlksubclwwlk  27208  eleclclwwlknlem2  27211  clwlksfclwwlkOLD  27235  clwlksf1clwwlklem0OLD  27237  clwwlknon1loop  27265  uhgr3cyclex  27354  eupth2lem3lem3  27402  eucrctshift  27415  eucrct2eupth1  27416  frgr3v  27449  3vfriswmgr  27452  1to3vfriswmgr  27454  3cyclfrgr  27462  frgrnbnb  27467  vdgn1frgrv2  27470  frgrwopreglem5  27495  frgrwopreglem5ALT  27496  fusgreghash2wspv  27509  frrusgrord0lem  27513  frrusgrord0  27514  2clwwlk2clwwlk  27526  extwwlkfab  27530  numclwwlk1lem2fo  27536  numclwwlk6  27577  frgrreggt1  27580  friendshipgt3  27585  ex-natded9.20-2  27605  grpoidinvlem3  27688  grpoidinv  27690  nmobndseqi  27961  nmobndseqiALT  27962  hvaddsub4  28262  hhcmpl  28384  ocsh  28469  5oalem2  28841  5oalem5  28844  3oalem2  28849  pjjsi  28886  hoadddir  28990  leopmul  29320  stge1i  29424  hatomistici  29548  mdsymlem2  29590  mdsymlem5  29593  addltmulALT  29632  isoun  29805  fsumiunle  29901  crefdf  30239  qqhre  30388  esumiun  30480  sxbrsigalem0  30657  dya2iocnei  30668  sxbrsigalem5  30674  sibfinima  30725  eulerpartlemgs2  30766  ballotlemfc0  30878  ballotlemfcc  30879  ballotlemsup  30890  bnj529  31132  bnj945  31165  bnj1098  31175  bnj1533  31243  bnj605  31298  bnj594  31303  bnj607  31307  bnj966  31335  bnj967  31336  bnj996  31346  bnj999  31348  bnj1006  31350  bnj1118  31373  bnj1172  31390  bnj1279  31407  bnj1296  31410  bnj1498  31450  cvmsi  31568  fv2ndcnv  31999  elno2  32126  trisegint  32454  funtransport  32457  btwnconn1lem4  32516  btwnconn2  32528  segcon2  32531  outsideofeu  32557  isfne  32653  lukshef-ax2  32729  limsucncmpi  32759  bj-restn0b  33353  bj-elid3  33401  bj-eldiag2  33407  unccur  33703  lindsenlbs  33715  matunitlindflem1  33716  matunitlindflem2  33717  poimirlem26  33746  poimirlem27  33747  poimirlem29  33749  poimirlem30  33750  poimirlem32  33752  heicant  33755  ismblfin  33761  itg2gt0cn  33775  bddiblnc  33790  areacirc  33815  opelopab3  33821  isdivrngo  34058  isdrngo2  34066  fldcrng  34112  flddmn  34166  cmtbr4N  35033  linepsubN  35530  pmapsub  35546  paddasslem14  35611  pclcmpatN  35679  trlval2  35941  cdleme20  36102  cdleme21j  36114  dvalveclem  36803  dia2dimlem7  36848  dvhlveclem  36886  docaclN  36902  dihjat1  37207  mapdhcl  37505  mapdh6dN  37517  mapdh8  37566  hdmap1l6d  37591  hdmap10  37618  hdmaprnlem17N  37641  hdmaplkr  37691  hdmapip0  37693  hgmapvv  37704  cmpfiiin  37759  pellexlem4  37895  pellqrex  37942  acongtr  38043  acongrep  38045  jm2.23  38061  rp-fakeanorass  38355  rp-isfinite6  38361  inintabss  38381  rfovcnvf1od  38795  clsk1indlem3  38838  ntrclsk13  38866  pm10.55  39065  refsum2cnlem1  39687  axccd2  39911  fmuldfeq  40292  climsuse  40317  limclner  40360  climxlim2lem  40548  icccncfext  40577  stoweidlem26  40719  stoweidlem52  40745  stoweidlem57  40750  fourierdlem20  40820  fourierdlem41  40841  fourierdlem52  40851  fourierdlem64  40863  fourierdlem102  40901  fourierdlem114  40913  ovolval4lem1  41342  preimagelt  41391  preimalegt  41392  funressneu  41663  afvelrn  41754  elfz2z  41897  2ffzoeq  41910  fargshiftfva  41951  ccatpfx  41981  pfxccat3  41998  pfxccatpfx2  42000  pfxccat3a  42001  reuccatpfxs1  42006  fmtnoprmfac1  42049  proththd  42103  opoeALTV  42166  evensumeven  42188  sbgoldbalt  42241  evengpop3  42258  evengpoap3  42259  nnsum4primeseven  42260  nnsum4primesevenALTV  42261  wtgoldbnnsum4prm  42262  bgoldbnnsum3prm  42264  tgoldbach  42277  uspgrsprfo  42321  assintop  42410  isringrng  42446  rnglz  42449  c0snmgmhm  42479  zrrnghm  42482  uzlidlring  42494  2zrngnmrid  42515  cznrng  42520  rnghmsubcsetclem2  42541  rhmsubcsetclem2  42587  rhmsubcrngclem2  42593  lmodvsmdi  42728  lincsum  42783  lincsumcl  42785  el0ldep  42820  ldepspr  42827  lindssnlvec  42840  modn0mul  42880  m1modmmod  42881  elbigolo1  42916  nn0digval  42959  setrec1lem3  43001  aacllem  43115
  Copyright terms: Public domain W3C validator