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

Theorem anim1i 589
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 587 1 ((𝜑𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  sylanl1  679  sylanr1  681  disamis  2559  rmob  3490  fores  6018  ssimaex  6154  dffv2  6162  exfo  6266  frnssb  6279  oprabv  6575  ndmovass  6693  fun11uni  6986  fabexg  6988  f1oabexg  6991  fun11iun  6992  soxp  7150  tz7.48lem  7396  tz7.49c  7401  omass  7520  oewordri  7532  omabs  7587  sbthlem9  7936  fineqvlem  8032  pssnn  8036  domunfican  8091  fiint  8095  fsuppsssupp  8147  sup0  8228  inf1  8375  infeq5  8390  cantnfle  8424  rankuni  8582  acndom  8730  acnnum  8731  cdainflem  8869  cfcof  8952  ac6num  9157  ac6s2  9164  brdom5  9205  brdom4  9206  genpnnp  9679  divmulasscom  10554  lediv2a  10762  supmul1  10835  infregelb  10850  nn2ge  10888  btwnz  11307  eluz2b2  11589  uz2mulcl  11594  eqreznegel  11602  xrsupexmnf  11959  xrinfmexpnf  11960  xrsupsslem  11961  xrinfmsslem  11962  supxrun  11970  ioo0  12023  elioo4g  12057  fz0fzelfz0  12265  fz0fzdiffz0  12268  2ffzeq  12280  elfzodifsumelfzo  12352  elfzom1elp1fzo  12353  zpnn0elfzo  12358  elfzom1elp1fzo1  12385  fzonfzoufzol  12388  quoremnn0  12468  zmodidfzoimp  12513  modabs  12516  modmuladd  12525  modifeq2int  12545  modaddmulmod  12550  expcl2lem  12685  iswrdsymb  13119  ccatcl  13154  ccatval3  13158  ccatalpha  13170  swrdfv2  13240  swrdsbslen  13242  swrdspsleq  13243  swrd0swrd  13255  swrdccatin2  13280  swrdccatin12lem3  13283  swrdccat3  13285  swrdccat3blem  13288  swrdccatid  13290  repswccat  13325  2cshw  13352  cshweqdifid  13359  lswco  13377  repsco  13378  s4f1o  13455  ccat2s1fvwALT  13488  trclun  13545  mulre  13651  rediv  13661  imdiv  13668  resqrex  13781  caurcvg2  14198  modfsummods  14308  tanval  14639  negdvdsb  14778  muldvds1  14786  muldvds2  14787  dvdscmulr  14790  dvdsmulcr  14791  dvdsdivcl  14818  nn0ehalf  14875  nn0oddm1d2  14881  nnoddm1d2  14882  sumeven  14890  sumodd  14891  divalglem8  14903  divgcdnn  15016  lcmfunsnlem2lem2  15132  lcmfun  15138  coprmgcdb  15142  ncoprmgcdne1b  15143  divgcdcoprm0  15159  maxprmfct  15201  ncoprmlnprm  15216  vfermltl  15286  vfermltlALT  15287  modprm0  15290  modprmn0modprm0  15292  pcpremul  15328  pcmul  15336  dvdsprmpweqle  15370  oddprmdvds  15387  prmdvdsprmo  15526  prmgaplem4  15538  prmgaplem7  15541  cshwsidrepsw  15580  gsmsymgreqlem2  17616  symgfixfo  17624  fsfnn0gsumfsffz  18144  irredn0  18468  rim0to0  18507  lsppratlem1  18910  ixpsnbasval  18972  cply1coe0bi  19433  dvdsrzring  19592  matinvgcell  19998  mat1dimcrng  20040  dmatscmcl  20066  scmatmats  20074  scmatscm  20076  scmatmulcl  20081  scmatghm  20096  scmatmhm  20097  ma1repvcl  20133  mdet1  20164  mdet0  20169  slesolinv  20243  slesolinvbi  20244  cramerimplem1  20246  cramerimp  20249  cramerlem1  20250  cramer  20254  cpmatacl  20278  cpmatmcl  20281  mat2pmatghm  20292  mat2pmatmul  20293  m2pmfzgsumcl  20310  decpmatmul  20334  decpmatmulsumfsupp  20335  pmatcollpwfi  20344  pmatcollpwscmat  20353  pm2mpf1  20361  pm2mpghm  20378  pm2mpmhmlem1  20380  monmat2matmon  20386  chpdmatlem2  20401  chpdmat  20403  chfacfisf  20416  cpmadugsumlemB  20436  cpmadugsumlemC  20437  cpmadugsumlemF  20438  clscld  20599  neiptopnei  20684  2ndcdisj2  21008  comppfsc  21083  tx1stc  21201  opnfbas  21394  fbasfip  21420  alexsublem  21596  alexsubALTlem4  21602  cnextcn  21619  cvsi  22663  bcthlem5  22846  vitalilem4  23099  vitalilem5  23100  itg2mulc  23233  dvcobr  23428  dvcnvlem  23456  dvferm1  23465  dvne0  23491  mdegmullem  23555  plyeq0lem  23683  plyexmo  23785  aalioulem5  23808  aalioulem6  23809  aaliou  23810  cxple2a  24158  cxpaddlelem  24205  cxpaddle  24206  relogbcxpb  24238  bcmono  24715  lgsprme0  24777  gausslemma2dlem0e  24798  gausslemma2dlem1a  24803  gausslemma2dlem6  24810  lgsquadlem2  24819  2lgsoddprm  24854  colinearalg  25504  axcontlem3  25560  usgraexmplef  25691  nb3grapr  25744  nb3grapr2  25745  nb3gra2nb  25746  cusgrarn  25750  cusgrasizeindslem2  25765  spthonepeq  25879  fargshiftfva  25929  wlkiswwlksur  26009  clwwlknimp  26066  clwlkisclwwlklem2a  26075  clwlkisclwwlklem0  26078  wwlksubclwwlk  26094  clwwisshclww  26097  clwwnisshclwwn  26099  eleclclwwlknlem2  26108  usg2spthonot1  26179  vdusgraval  26196  cusgraisrusgra  26227  rusgranumwlk  26246  eupatrl  26257  1to3vfriswmgra  26296  frgranbnb  26309  vdfrgra0  26311  vdgn0frgrav2  26313  vdgn1frgrav2  26315  frgrawopreg  26338  frg2wot1  26346  usg2spot2nb  26354  frgraregorufrg  26361  numclwwlkovfel2  26372  numclwlk1lem2foa  26380  numclwlk1lem2fv  26382  numclwwlk1  26387  numclwlk2lem2fv  26393  numclwwlk4  26399  numclwwlk5  26401  numclwwlk6  26402  frgrareg  26406  frgraregord013  26407  ex-natded9.20-2  26429  grpoidinvlem3  26506  grpoidinv  26508  sspival  26777  nmobndseqi  26820  nmobndseqiALT  26821  hvaddsub4  27121  hhcmpl  27243  ocsh  27328  5oalem2  27700  5oalem5  27703  3oalem2  27708  pjjsi  27745  hoadddir  27849  leopmul  28179  stge1i  28283  hatomistici  28407  mdsymlem2  28449  mdsymlem5  28452  addltmulALT  28491  isoun  28664  crefdf  29045  qqhre  29194  esumiun  29285  sxbrsigalem0  29462  dya2iocnei  29473  sxbrsigalem5  29479  sibfinima  29530  eulerpartlemgs2  29571  ballotlemfc0  29683  ballotlemfcc  29684  ballotlemsup  29695  bnj529  29867  bnj945  29900  bnj1098  29910  bnj1533  29978  bnj605  30033  bnj594  30038  bnj607  30042  bnj966  30070  bnj967  30071  bnj996  30081  bnj999  30083  bnj1006  30085  bnj1118  30108  bnj1172  30125  bnj1279  30142  bnj1296  30145  bnj1498  30185  cvmsi  30303  fv2ndcnv  30728  elno2  30853  nobndlem6  30898  trisegint  31107  funtransport  31110  btwnconn1lem4  31169  btwnconn2  31181  segcon2  31184  outsideofeu  31210  isfne  31306  lukshef-ax2  31386  limsucncmpi  31416  bj-restn0b  32024  bj-elid3  32063  bj-eldiag2  32068  unccur  32361  lindsenlbs  32373  matunitlindflem1  32374  matunitlindflem2  32375  poimirlem26  32404  poimirlem27  32405  poimirlem29  32407  poimirlem30  32408  poimirlem32  32410  heicant  32413  ismblfin  32419  itg2gt0cn  32434  bddiblnc  32449  areacirc  32474  opelopab3  32480  isdivrngo  32718  isdrngo2  32726  fldcrng  32772  flddmn  32826  cmtbr4N  33359  linepsubN  33855  pmapsub  33871  paddasslem14  33936  pclcmpatN  34004  trlval2  34267  cdleme20  34429  cdleme21j  34441  dvalveclem  35131  dia2dimlem7  35176  dvhlveclem  35214  docaclN  35230  dihjat1  35535  mapdhcl  35833  mapdh6dN  35845  mapdh8  35895  hdmap1l6d  35920  hdmap10  35949  hdmaprnlem17N  35972  hdmaplkr  36022  hdmapip0  36024  hgmapvv  36035  cmpfiiin  36077  pellexlem4  36213  pellqrex  36260  acongtr  36362  acongrep  36364  jm2.23  36380  rp-fakeanorass  36676  rp-isfinite6  36682  inintabss  36702  rfovcnvf1od  37117  clsk1indlem3  37160  ntrclsk13  37188  pm10.55  37389  refsum2cnlem1  38018  axccd2  38224  fmuldfeq  38450  climsuse  38475  limclner  38518  icccncfext  38573  stoweidlem26  38719  stoweidlem52  38745  stoweidlem57  38750  fourierdlem20  38820  fourierdlem41  38841  fourierdlem52  38851  fourierdlem64  38863  fourierdlem102  38901  fourierdlem114  38913  ovolval4lem1  39339  preimagelt  39389  preimalegt  39390  afvelrn  39698  fmtnoprmfac1  39816  proththd  39870  opoeALTV  39933  evensumeven  39955  sgoldbalt  40004  evengpop3  40015  evengpoap3  40016  nnsum4primeseven  40017  nnsum4primesevenALTV  40018  wtgoldbnnsum4prm  40019  bgoldbnnsum3prm  40021  tgoldbach  40033  tgoldbachOLD  40040  ccatpfx  40073  pfxccat3  40090  pfxccatpfx2  40092  pfxccat3a  40093  reuccatpfxs1  40098  elpwdifsn  40113  fpropnf1  40160  elfz2z  40175  2ffzoeq  40184  uhgrstrrepelem  40301  umgrislfupgrlem  40345  edgupgr  40365  usgruspgrb  40409  usgrislfuspgr  40412  edgassv2  40423  umgr2edg  40434  usgr2edg  40435  uspgredg2v  40449  subupgr  40509  subusgr  40511  usgrfilem  40544  nbupgrres  40590  nb3gr2nb  40610  nbupgruvtxres  40632  cplgr3v  40655  cusgrres  40662  cusgrsizeindslem  40665  cusgrsizeinds  40666  vtxdun  40694  finrusgrfusgr  40763  cusgrrusgr  40779  wlkOnprop  40864  1wlkreslem  40876  trlsonprop  40913  spthdep  40938  pthsonprop  40948  spthonprop  40949  spthonepeq-av  40956  uhgr1wlkspth  40959  usgr2wlkspth  40963  crctcsh1wlkn0lem6  41016  crctcsh1wlkn0lem7  41017  crctcshtrl  41024  crctcsh  41025  wlkwwlksur  41092  umgr2adedgwlkonALT  41152  elwwlks2  41168  elwspths2spth  41169  rusgrnumwwlk  41176  clwwlknbp0  41190  clwlkclwwlklem2a  41205  clwlkclwwlklem3  41208  clwwlksnfi  41218  wwlksext2clwwlk  41229  wwlksubclwwlks  41230  clwwisshclwws  41233  eleclclwwlksnlem2  41244  clwlksfclwwlk  41267  clwlksf1clwwlklem0  41269  uhgr3cyclex  41347  eupth2lem3lem3  41396  eucrctshift  41409  eucrct2eupth1  41410  frgr3v  41443  3vfriswmgr  41446  1to3vfriswmgr  41448  3cyclfrgr  41456  frgrnbnb  41461  vdgn1frgrv2  41464  frgrwopreg  41484  fusgr2wsp2nb  41496  fusgreghash2wspv  41497  frrusgrord0  41501  frgrregorufrg  41503  av-numclwlk1lem2foa  41519  av-numclwwlk4  41538  av-numclwwlk6  41542  av-frgrareggt1  41545  av-friendshipgt3  41550  assintop  41633  isringrng  41669  rnglz  41672  c0snmgmhm  41702  zrrnghm  41705  uzlidlring  41717  2zrngnmrid  41738  cznrng  41745  rnghmsubcsetclem2  41766  rhmsubcsetclem2  41812  rhmsubcrngclem2  41818  lmodvsmdi  41955  lincsum  42010  lincsumcl  42012  el0ldep  42047  ldepspr  42054  lindssnlvec  42067  modn0mul  42107  m1modmmod  42108  elbigolo1  42147  nn0digval  42190  aacllem  42315
  Copyright terms: Public domain W3C validator