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

Theorem anim1i 568
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 566 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sylanl1  650  sylanr1  652  disamis  2409  fores  5809  ssimaex  5938  dffv2  5946  exfo  6049  oprabv  6345  ndmovass  6463  fun11uni  6754  fabexg  6756  f1oabexg  6759  fun11iun  6760  soxp  6913  tz7.48lem  7125  tz7.49c  7130  omass  7248  oewordri  7260  omabs  7315  sbthlem9  7655  fineqvlem  7754  pssnn  7758  domunfican  7813  fiint  7817  fsuppsssupp  7865  inf1  8060  infeq5  8075  cantnfle  8111  rankuni  8302  acndom  8453  acnnum  8454  cdainflem  8592  cfcof  8675  ac6num  8880  ac6s2  8887  brdom5  8928  brdom4  8929  genpnnp  9404  lediv2a  10464  supmul1  10533  nn2ge  10586  btwnz  10991  eluz2b2  11183  uz2mulcl  11188  eqreznegel  11196  xrsupexmnf  11525  xrinfmexpnf  11526  xrsupsslem  11527  xrinfmsslem  11528  supxrun  11536  ioo0  11583  elioo4g  11614  fz0fzelfz0  11809  fz0fzdiffz0  11812  2ffzeq  11823  elfzodifsumelfzo  11882  elfzom1elp1fzo  11883  zpnn0elfzo  11888  fzonfzoufzol  11913  quoremnn0  11983  zmodidfzoimp  12026  modabs  12029  modifeq2int  12049  modaddmulmod  12053  expcl2lem  12178  ccatw2s1p1  12640  ccatw2s1p2  12641  swrdspsleq  12673  swrd0swrd  12686  swrdccatin2  12712  swrdccatin12lem3  12715  swrdccat3  12717  swrdccat3blem  12720  swrdccatid  12722  repswccat  12757  2cshw  12781  cshweqdifid  12788  lswco  12804  repsco  12805  s4f1o  12866  ccat2s1fvwALT  12893  mulre  12954  rediv  12964  imdiv  12971  resqrex  13084  caurcvg2  13500  modfsummods  13607  tanval  13863  negdvdsb  14000  muldvds1  14008  muldvds2  14009  dvdscmulr  14012  dvdsmulcr  14013  divalglem8  14058  maxprmfct  14254  modprm0  14330  modprmn0modprm0  14332  pcpremul  14367  pcmul  14375  cshwsidrepsw  14578  gsmsymgreqlem2  16456  symgfixfo  16464  fsfnn0gsumfsffz  17011  irredn0  17352  rim0to0  17391  lsppratlem1  17793  ixpsnbasval  17855  cply1coe0bi  18342  dvdsrzring  18507  dvdsrz  18508  matinvgcell  18937  mat1dimcrng  18979  dmatscmcl  19005  scmatmats  19013  scmatscm  19015  scmatmulcl  19020  scmatghm  19035  scmatmhm  19036  ma1repvcl  19072  mdet1  19103  mdet0  19108  slesolinv  19182  slesolinvbi  19183  cramerimplem1  19185  cramerimp  19188  cramerlem1  19189  cramer  19193  cpmatacl  19217  cpmatmcl  19220  mat2pmatghm  19231  mat2pmatmul  19232  m2pmfzgsumcl  19249  decpmatmul  19273  decpmatmulsumfsupp  19274  pmatcollpwfi  19283  pmatcollpwscmat  19292  pm2mpf1  19300  pm2mpghm  19317  pm2mpmhmlem1  19319  monmat2matmon  19325  chpdmatlem2  19340  chpdmat  19342  chfacfisf  19355  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  clscld  19548  neiptopnei  19633  2ndcdisj2  19958  comppfsc  20033  tx1stc  20151  opnfbas  20343  fbasfip  20369  alexsublem  20544  alexsubALTlem4  20550  cnextcn  20567  bcthlem5  21767  vitalilem4  22020  vitalilem5  22021  itg2mulc  22154  dvcobr  22349  dvcnvlem  22377  dvferm1  22386  dvne0  22412  mdegmullem  22478  plyeq0lem  22607  plyexmo  22709  aalioulem5  22732  aalioulem6  22733  aaliou  22734  cxple2a  23080  cxpaddlelem  23125  cxpaddle  23126  bcmono  23552  lgsquadlem2  23630  colinearalg  24213  axcontlem3  24269  usgraexmpl  24401  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgrarn  24459  cusgrasizeindslem3  24475  spthonepeq  24589  fargshiftfva  24639  wlkiswwlksur  24719  clwwlknimp  24776  clwlkisclwwlklem2a  24785  clwlkisclwwlklem0  24788  wwlksubclwwlk  24804  clwwisshclww  24807  clwwnisshclwwn  24809  eleclclwwlknlem2  24818  usg2spthonot1  24890  vdusgraval  24907  cusgraisrusgra  24938  rusgranumwlk  24957  eupatrl  24968  1to3vfriswmgra  25007  frgranbnb  25020  vdfrgra0  25022  vdgn0frgrav2  25024  vdgn1frgrav2  25026  frgrawopreg  25049  frg2wot1  25057  usg2spot2nb  25065  frgraregorufrg  25072  numclwwlkovfel2  25083  numclwlk1lem2foa  25091  numclwlk1lem2fv  25093  numclwwlk1  25098  numclwlk2lem2fv  25104  numclwwlk4  25110  numclwwlk5  25112  numclwwlk6  25113  frgrareg  25117  frgraregord013  25118  ex-natded9.20-2  25139  grpoidinvlem3  25208  grpoidinv  25210  isdivrngo  25433  sspival  25651  nmobndseqi  25694  nmobndseqiOLD  25695  hvaddsub4  25995  hhcmpl  26117  ocsh  26201  5oalem2  26573  5oalem5  26576  3oalem2  26581  pjjsi  26618  hoadddir  26723  leopmul  27053  stge1i  27157  hatomistici  27281  mdsymlem2  27323  mdsymlem5  27326  addltmulALT  27365  isoun  27520  crefdf  27851  qqhre  27998  sxbrsigalem0  28242  dya2iocnei  28253  sxbrsigalem5  28259  sibfinima  28281  eulerpartlemgs2  28319  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsup  28443  cvmsi  28710  elno2  29414  nobndlem6  29457  trisegint  29678  funtransport  29681  btwnconn1lem4  29740  btwnconn2  29752  segcon2  29755  outsideofeu  29781  lukshef-ax2  29880  limsucncmpi  29910  heicant  30049  ismblfin  30055  itg2gt0cn  30070  bddiblnc  30085  areacirc  30112  isfne  30157  opelopab3  30207  isdrngo2  30361  fldcrng  30401  flddmn  30455  cmpfiiin  30629  pellexlem4  30768  pellqrex  30815  acongtr  30916  acongrep  30918  jm2.23  30938  pm10.55  31274  refsum2cnlem1  31412  fmuldfeq  31577  climsuse  31614  limclner  31657  icccncfext  31690  stoweidlem26  31808  stoweidlem52  31834  stoweidlem57  31839  fourierdlem20  31909  fourierdlem41  31930  fourierdlem52  31941  fourierdlem64  31953  fourierdlem102  31991  fourierdlem114  32003  afvelrn  32253  elpwdifsn  32296  lesubnn0  32326  elfz2z  32331  2ffzoeq  32341  edgssv2ALT  32401  edgssv2  32402  usgfislem2  32445  usgfisALTlem2  32449  assintop  32533  isringrng  32687  rnglz  32690  c0snmgmhm  32720  zrrnghm  32723  uzlidlring  32735  2zrngnmrid  32756  cznrng  32763  rnghmsubcsetclem2  32784  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  lmodvsmdi  32975  lincsum  33030  lincsumcl  33032  el0ldep  33067  ldepspr  33074  lindssnlvec  33087  aacllem  33216  bnj529  33798  bnj945  33832  bnj1098  33842  bnj1533  33910  bnj605  33965  bnj594  33970  bnj607  33974  bnj966  34002  bnj967  34003  bnj996  34013  bnj999  34015  bnj1006  34017  bnj1118  34040  bnj1172  34057  bnj1279  34074  bnj1296  34077  bnj1498  34117  bj-elid3  34601  bj-eldiag2  34607  cmtbr4N  34980  linepsubN  35476  pmapsub  35492  paddasslem14  35557  pclcmpatN  35625  trlval2  35888  cdleme20  36050  cdleme21j  36062  dvalveclem  36752  dia2dimlem7  36797  dvhlveclem  36835  docaclN  36851  dihjat1  37156  mapdhcl  37454  mapdh6dN  37466  mapdh8  37516  hdmap1l6d  37541  hdmap10  37570  hdmaprnlem17N  37593  hdmaplkr  37643  hdmapip0  37645  hgmapvv  37656  rp-fakeanorass  37737  rp-isfinite6  37744
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