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

Theorem anim1i 591
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 589 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 197  df-an 386
This theorem is referenced by:  sylanl1  681  sylanr1  683  disamis  2574  rmob  3522  eqeuel  3932  elpwdifsn  4310  fores  6111  ssimaex  6250  dffv2  6258  exfo  6363  frnssb  6377  fpropnf1  6509  oprabv  6688  ndmovass  6807  fun11uni  7105  fabexg  7107  f1oabexg  7110  fun11iun  7111  soxp  7275  tz7.48lem  7521  tz7.49c  7526  omass  7645  oewordri  7657  omabs  7712  sbthlem9  8063  fineqvlem  8159  pssnn  8163  domunfican  8218  fiint  8222  fsuppsssupp  8276  sup0  8357  inf1  8504  infeq5  8519  cantnfle  8553  rankuni  8711  acndom  8859  acnnum  8860  cdainflem  8998  cfcof  9081  ac6num  9286  ac6s2  9293  brdom5  9336  brdom4  9337  genpnnp  9812  divmulasscom  10694  lediv2a  10902  supmul1  10977  infregelb  10992  nn2ge  11030  btwnz  11464  eluz2b2  11746  uz2mulcl  11751  eqreznegel  11759  xrsupexmnf  12120  xrinfmexpnf  12121  xrsupsslem  12122  xrinfmsslem  12123  supxrun  12131  ioo0  12185  elioo4g  12219  fz0fzelfz0  12429  fz0fzdiffz0  12432  2ffzeq  12444  elfzodifsumelfzo  12517  elfzom1elp1fzo  12518  zpnn0elfzo  12524  elfzom1elp1fzo1  12552  fzonfzoufzol  12555  quoremnn0  12638  zmodidfzoimp  12683  modabs  12686  modmuladd  12695  modifeq2int  12715  modaddmulmod  12720  expcl2lem  12855  hashreshashfun  13209  iswrdsymb  13305  ccatcl  13342  ccatval3  13346  ccatalpha  13358  swrdfv2  13428  swrdsbslen  13430  swrdspsleq  13431  swrd0swrd  13443  swrdccatin2  13468  swrdccatin12lem3  13471  swrdccat3  13473  swrdccat3blem  13476  swrdccatid  13478  repswccat  13513  2cshw  13540  cshweqdifid  13547  lswco  13565  repsco  13566  s4f1o  13644  ccat2s1fvwALT  13679  trclun  13736  mulre  13842  rediv  13852  imdiv  13859  resqrex  13972  caurcvg2  14389  fsumdifsnconst  14504  modfsummods  14506  tanval  14839  negdvdsb  14979  muldvds1  14987  muldvds2  14988  dvdscmulr  14991  dvdsmulcr  14992  dvdsdivcl  15019  nn0ehalf  15076  nn0oddm1d2  15082  nnoddm1d2  15083  sumeven  15091  sumodd  15092  divalglem8  15104  divgcdnn  15217  lcmfunsnlem2lem2  15333  lcmfun  15339  coprmgcdb  15343  ncoprmgcdne1b  15344  divgcdcoprm0  15360  maxprmfct  15402  ncoprmlnprm  15417  vfermltl  15487  vfermltlALT  15488  modprm0  15491  modprmn0modprm0  15493  pcpremul  15529  pcmul  15537  dvdsprmpweqle  15571  oddprmdvds  15588  prmdvdsprmo  15727  prmgaplem4  15739  prmgaplem7  15742  cshwsidrepsw  15781  gsmsymgreqlem2  17832  symgfixfo  17840  fsfnn0gsumfsffz  18360  irredn0  18684  rim0to0  18723  lsppratlem1  19128  ixpsnbasval  19190  cply1coe0bi  19651  dvdsrzring  19812  matinvgcell  20222  mat1dimcrng  20264  dmatscmcl  20290  scmatmats  20298  scmatscm  20300  scmatmulcl  20305  scmatghm  20320  scmatmhm  20321  ma1repvcl  20357  mdet1  20388  mdet0  20393  slesolinv  20467  slesolinvbi  20468  cramerimplem1  20470  cramerimp  20473  cramerlem1  20474  cramer  20478  cpmatacl  20502  cpmatmcl  20505  mat2pmatghm  20516  mat2pmatmul  20517  m2pmfzgsumcl  20534  decpmatmul  20558  decpmatmulsumfsupp  20559  pmatcollpwfi  20568  pmatcollpwscmat  20577  pm2mpf1  20585  pm2mpghm  20602  pm2mpmhmlem1  20604  monmat2matmon  20610  chpdmatlem2  20625  chpdmat  20627  chfacfisf  20640  cpmadugsumlemB  20660  cpmadugsumlemC  20661  cpmadugsumlemF  20662  clscld  20832  neiptopnei  20917  2ndcdisj2  21241  comppfsc  21316  tx1stc  21434  opnfbas  21627  fbasfip  21653  alexsublem  21829  alexsubALTlem4  21835  cnextcn  21852  ngpocelbl  22489  cvsi  22911  cphipval  23023  bcthlem5  23106  vitalilem4  23361  vitalilem5  23362  itg2mulc  23495  dvcobr  23690  dvcnvlem  23720  dvferm1  23729  dvne0  23755  mdegmullem  23819  plyeq0lem  23947  plyexmo  24049  aalioulem5  24072  aalioulem6  24073  aaliou  24074  cxple2a  24426  cxpaddlelem  24473  cxpaddle  24474  relogbcxpb  24506  bcmono  24983  lgsprme0  25045  gausslemma2dlem0e  25066  gausslemma2dlem1a  25071  gausslemma2dlem6  25078  lgsquadlem2  25087  2lgsoddprm  25122  colinearalg  25771  axcontlem3  25827  umgrislfupgrlem  25998  edgupgr  26010  usgruspgrb  26057  usgrislfuspgr  26060  edgssv2  26071  umgr2edg  26082  usgr2edg  26083  uspgredg2v  26097  usgrexmplef  26132  subupgr  26160  subusgr  26162  usgrfilem  26200  nbupgrres  26247  nb3gr2nb  26267  nbupgruvtxres  26289  cplgr3v  26312  cusgrres  26325  cusgrsizeindslem  26328  cusgrsizeinds  26329  vtxdun  26358  finrusgrfusgr  26442  cusgrrusgr  26458  wlkonprop  26535  wlkreslem  26547  trlsonprop  26585  spthdep  26611  pthsonprop  26621  spthonprop  26622  cycliscrct  26675  crctcshwlkn0lem6  26688  crctcshwlkn0lem7  26689  crctcshtrl  26696  crctcsh  26697  wlkwwlksur  26764  umgr2adedgwlkonALT  26824  elwwlks2  26842  elwspths2spth  26843  rusgrnumwwlk  26851  clwwlknbp0  26865  clwlkclwwlklem2a  26880  clwlkclwwlklem3  26883  clwwlksnfi  26893  wwlksext2clwwlk  26904  wwlksubclwwlks  26905  clwwisshclwws  26908  eleclclwwlksnlem2  26919  clwlksfclwwlk  26942  clwlksf1clwwlklem0  26944  uhgr3cyclex  27022  eupth2lem3lem3  27070  eucrctshift  27083  eucrct2eupth1  27084  frgr3v  27119  3vfriswmgr  27122  1to3vfriswmgr  27124  3cyclfrgr  27132  frgrnbnb  27137  vdgn1frgrv2  27140  fusgreghash2wspv  27173  frrusgrord0lem  27177  frrusgrord0  27178  numclwlk1lem2foa  27195  numclwwlk4  27214  numclwwlk6  27218  frgrreggt1  27221  friendshipgt3  27226  ex-natded9.20-2  27245  grpoidinvlem3  27330  grpoidinv  27332  nmobndseqi  27604  nmobndseqiALT  27605  hvaddsub4  27905  hhcmpl  28027  ocsh  28112  5oalem2  28484  5oalem5  28487  3oalem2  28492  pjjsi  28529  hoadddir  28633  leopmul  28963  stge1i  29067  hatomistici  29191  mdsymlem2  29233  mdsymlem5  29236  addltmulALT  29275  isoun  29453  fsumiunle  29549  crefdf  29889  qqhre  30038  esumiun  30130  sxbrsigalem0  30307  dya2iocnei  30318  sxbrsigalem5  30324  sibfinima  30375  eulerpartlemgs2  30416  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemsup  30540  bnj529  30785  bnj945  30818  bnj1098  30828  bnj1533  30896  bnj605  30951  bnj594  30956  bnj607  30960  bnj966  30988  bnj967  30989  bnj996  30999  bnj999  31001  bnj1006  31003  bnj1118  31026  bnj1172  31043  bnj1279  31060  bnj1296  31063  bnj1498  31103  cvmsi  31221  fv2ndcnv  31655  elno2  31781  trisegint  32110  funtransport  32113  btwnconn1lem4  32172  btwnconn2  32184  segcon2  32187  outsideofeu  32213  isfne  32309  lukshef-ax2  32389  limsucncmpi  32419  bj-restn0b  33019  bj-elid3  33058  bj-eldiag2  33063  unccur  33363  lindsenlbs  33375  matunitlindflem1  33376  matunitlindflem2  33377  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem30  33410  poimirlem32  33412  heicant  33415  ismblfin  33421  itg2gt0cn  33436  bddiblnc  33451  areacirc  33476  opelopab3  33482  isdivrngo  33720  isdrngo2  33728  fldcrng  33774  flddmn  33828  cmtbr4N  34361  linepsubN  34857  pmapsub  34873  paddasslem14  34938  pclcmpatN  35006  trlval2  35269  cdleme20  35431  cdleme21j  35443  dvalveclem  36133  dia2dimlem7  36178  dvhlveclem  36216  docaclN  36232  dihjat1  36537  mapdhcl  36835  mapdh6dN  36847  mapdh8  36897  hdmap1l6d  36922  hdmap10  36951  hdmaprnlem17N  36974  hdmaplkr  37024  hdmapip0  37026  hgmapvv  37037  cmpfiiin  37079  pellexlem4  37215  pellqrex  37262  acongtr  37364  acongrep  37366  jm2.23  37382  rp-fakeanorass  37677  rp-isfinite6  37683  inintabss  37703  rfovcnvf1od  38118  clsk1indlem3  38161  ntrclsk13  38189  pm10.55  38388  refsum2cnlem1  39016  axccd2  39246  fmuldfeq  39615  climsuse  39640  limclner  39683  icccncfext  39863  stoweidlem26  40006  stoweidlem52  40032  stoweidlem57  40037  fourierdlem20  40107  fourierdlem41  40128  fourierdlem52  40138  fourierdlem64  40150  fourierdlem102  40188  fourierdlem114  40200  ovolval4lem1  40626  preimagelt  40675  preimalegt  40676  afvelrn  41011  elfz2z  41088  2ffzoeq  41101  fargshiftfva  41143  ccatpfx  41174  pfxccat3  41191  pfxccatpfx2  41193  pfxccat3a  41194  reuccatpfxs1  41199  fmtnoprmfac1  41242  proththd  41296  opoeALTV  41359  evensumeven  41381  sbgoldbalt  41434  evengpop3  41451  evengpoap3  41452  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  tgoldbach  41470  tgoldbachOLD  41477  uspgrsprfo  41521  assintop  41610  isringrng  41646  rnglz  41649  c0snmgmhm  41679  zrrnghm  41682  uzlidlring  41694  2zrngnmrid  41715  cznrng  41720  rnghmsubcsetclem2  41741  rhmsubcsetclem2  41787  rhmsubcrngclem2  41793  lmodvsmdi  41928  lincsum  41983  lincsumcl  41985  el0ldep  42020  ldepspr  42027  lindssnlvec  42040  modn0mul  42080  m1modmmod  42081  elbigolo1  42116  nn0digval  42159  setrec1lem3  42201  aacllem  42312
  Copyright terms: Public domain W3C validator