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 383
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 385
This theorem is referenced by:  sylanl1  683  sylanr1  685  disamis  2605  rmob  3562  eqeuel  3974  elpwdifsn  4352  fores  6162  ssimaex  6302  dffv2  6310  exfo  6417  frnssb  6431  fpropnf1  6564  oprabv  6745  ndmovass  6864  fun11uni  7162  fabexg  7164  f1oabexg  7167  fun11iun  7168  soxp  7335  tz7.48lem  7581  tz7.49c  7586  omass  7705  oewordri  7717  omabs  7772  sbthlem9  8119  fineqvlem  8215  pssnn  8219  domunfican  8274  fiint  8278  fsuppsssupp  8332  sup0  8413  inf1  8557  infeq5  8572  cantnfle  8606  rankuni  8764  acndom  8912  acnnum  8913  cdainflem  9051  cfcof  9134  ac6num  9339  ac6s2  9346  brdom5  9389  brdom4  9390  genpnnp  9865  divmulasscom  10747  lediv2a  10955  supmul1  11030  infregelb  11045  nn2ge  11083  btwnz  11517  eluz2b2  11799  uz2mulcl  11804  eqreznegel  11812  xrsupexmnf  12173  xrinfmexpnf  12174  xrsupsslem  12175  xrinfmsslem  12176  supxrun  12184  ioo0  12238  elioo4g  12272  fz0fzelfz0  12484  fz0fzdiffz0  12487  2ffzeq  12499  elfzodifsumelfzo  12573  elfzom1elp1fzo  12574  zpnn0elfzo  12580  elfzom1elp1fzo1  12608  fzonfzoufzol  12611  quoremnn0  12695  zmodidfzoimp  12740  modabs  12743  modmuladd  12752  modifeq2int  12772  modaddmulmod  12777  expcl2lem  12912  hashreshashfun  13264  iswrdsymb  13354  ccatcl  13392  ccatval3  13397  ccatalpha  13411  swrdfv2  13492  swrdsbslen  13494  swrdspsleq  13495  swrd0swrd  13507  swrdccatin2  13533  swrdccatin12lem3  13536  swrdccat3  13538  swrdccat3blem  13541  swrdccatid  13543  repswccat  13578  2cshw  13605  cshweqdifid  13612  lswco  13630  repsco  13631  s4f1o  13709  ccat2s1fvwALT  13744  trclun  13799  mulre  13905  rediv  13915  imdiv  13922  resqrex  14035  caurcvg2  14452  fsumdifsnconst  14567  modfsummods  14569  tanval  14902  p1modz1  15034  negdvdsb  15045  muldvds1  15053  muldvds2  15054  dvdscmulr  15057  dvdsmulcr  15058  dvdsdivcl  15085  nn0ehalf  15142  nn0oddm1d2  15148  nnoddm1d2  15149  sumeven  15157  sumodd  15158  divalglem8  15170  divgcdnn  15283  lcmfunsnlem2lem2  15399  lcmfun  15405  coprmgcdb  15409  ncoprmgcdne1b  15410  divgcdcoprm0  15426  maxprmfct  15468  ncoprmlnprm  15483  vfermltl  15553  vfermltlALT  15554  modprm0  15557  modprmn0modprm0  15559  pcpremul  15595  pcmul  15603  dvdsprmpweqle  15637  oddprmdvds  15654  prmdvdsprmo  15793  prmgaplem4  15805  prmgaplem7  15808  cshwsidrepsw  15847  gsmsymgreqlem2  17897  symgfixfo  17905  fsfnn0gsumfsffz  18425  irredn0  18749  rim0to0  18790  lsppratlem1  19195  ixpsnbasval  19257  cply1coe0bi  19718  dvdsrzring  19879  matinvgcell  20289  mat1dimcrng  20331  dmatscmcl  20357  scmatmats  20365  scmatscm  20367  scmatmulcl  20372  scmatghm  20387  scmatmhm  20388  ma1repvcl  20424  mdet1  20455  mdet0  20460  slesolinv  20534  slesolinvbi  20535  cramerimplem1  20537  cramerimp  20540  cramerlem1  20541  cramer  20545  cpmatacl  20569  cpmatmcl  20572  mat2pmatghm  20583  mat2pmatmul  20584  m2pmfzgsumcl  20601  decpmatmul  20625  decpmatmulsumfsupp  20626  pmatcollpwfi  20635  pmatcollpwscmat  20644  pm2mpf1  20652  pm2mpghm  20669  pm2mpmhmlem1  20671  monmat2matmon  20677  chpdmatlem2  20692  chpdmat  20694  chfacfisf  20707  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  clscld  20899  neiptopnei  20984  2ndcdisj2  21308  comppfsc  21383  tx1stc  21501  opnfbas  21693  fbasfip  21719  alexsublem  21895  alexsubALTlem4  21901  cnextcn  21918  ngpocelbl  22555  cvsi  22976  cphipval  23088  bcthlem5  23171  vitalilem4  23425  vitalilem5  23426  itg2mulc  23559  dvcobr  23754  dvcnvlem  23784  dvferm1  23793  dvne0  23819  mdegmullem  23883  plyeq0lem  24011  plyexmo  24113  aalioulem5  24136  aalioulem6  24137  aaliou  24138  cxple2a  24490  cxpaddlelem  24537  cxpaddle  24538  relogbcxpb  24570  bcmono  25047  lgsprme0  25109  gausslemma2dlem0e  25130  gausslemma2dlem1a  25135  gausslemma2dlem6  25142  lgsquadlem2  25151  2lgsoddprm  25186  colinearalg  25835  axcontlem3  25891  umgrislfupgrlem  26062  edgupgr  26074  usgruspgrb  26121  usgrislfuspgr  26124  edgssv2  26135  umgr2edg  26146  usgr2edg  26147  uspgredg2v  26161  usgrexmplef  26196  subupgr  26224  subusgr  26226  usgrfilem  26264  nbupgrres  26310  nb3gr2nb  26330  nbupgruvtxres  26358  cplgr3v  26387  cusgrres  26400  cusgrsizeindslem  26403  cusgrsizeinds  26404  vtxdun  26433  finrusgrfusgr  26517  cusgrrusgr  26533  wlkonprop  26610  wlkreslem  26622  trlsonprop  26660  spthdep  26686  pthsonprop  26696  spthonprop  26697  cycliscrct  26750  crctcshwlkn0lem6  26763  crctcshwlkn0lem7  26764  crctcshtrl  26771  crctcsh  26772  wlkwwlksur  26851  umgr2adedgwlkonALT  26912  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlk  26942  clwlkclwwlklem2a  26964  clwlkclwwlklem3  26967  clwwisshclwws  26972  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  eleclclwwlknlem2  27026  clwlksfclwwlk  27049  clwlksf1clwwlklem0  27051  clwwlknon1loop  27073  uhgr3cyclex  27160  eupth2lem3lem3  27208  eucrctshift  27221  eucrct2eupth1  27222  frgr3v  27255  3vfriswmgr  27258  1to3vfriswmgr  27260  3cyclfrgr  27268  frgrnbnb  27273  vdgn1frgrv2  27276  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  fusgreghash2wspv  27315  frrusgrord0lem  27319  frrusgrord0  27320  clwwlkccatlem  27331  extwwlkfab  27342  numclwlk1lem2fo  27348  numclwwlk6  27377  frgrreggt1  27380  friendshipgt3  27385  ex-natded9.20-2  27405  grpoidinvlem3  27488  grpoidinv  27490  nmobndseqi  27762  nmobndseqiALT  27763  hvaddsub4  28063  hhcmpl  28185  ocsh  28270  5oalem2  28642  5oalem5  28645  3oalem2  28650  pjjsi  28687  hoadddir  28791  leopmul  29121  stge1i  29225  hatomistici  29349  mdsymlem2  29391  mdsymlem5  29394  addltmulALT  29433  isoun  29607  fsumiunle  29703  crefdf  30043  qqhre  30192  esumiun  30284  sxbrsigalem0  30461  dya2iocnei  30472  sxbrsigalem5  30478  sibfinima  30529  eulerpartlemgs2  30570  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsup  30694  bnj529  30937  bnj945  30970  bnj1098  30980  bnj1533  31048  bnj605  31103  bnj594  31108  bnj607  31112  bnj966  31140  bnj967  31141  bnj996  31151  bnj999  31153  bnj1006  31155  bnj1118  31178  bnj1172  31195  bnj1279  31212  bnj1296  31215  bnj1498  31255  cvmsi  31373  fv2ndcnv  31805  elno2  31932  trisegint  32260  funtransport  32263  btwnconn1lem4  32322  btwnconn2  32334  segcon2  32337  outsideofeu  32363  isfne  32459  lukshef-ax2  32539  limsucncmpi  32569  bj-restn0b  33169  bj-elid3  33217  bj-eldiag2  33222  unccur  33522  lindsenlbs  33534  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem30  33569  poimirlem32  33571  heicant  33574  ismblfin  33580  itg2gt0cn  33595  bddiblnc  33610  areacirc  33635  opelopab3  33641  isdivrngo  33879  isdrngo2  33887  fldcrng  33933  flddmn  33987  cmtbr4N  34860  linepsubN  35356  pmapsub  35372  paddasslem14  35437  pclcmpatN  35505  trlval2  35768  cdleme20  35929  cdleme21j  35941  dvalveclem  36631  dia2dimlem7  36676  dvhlveclem  36714  docaclN  36730  dihjat1  37035  mapdhcl  37333  mapdh6dN  37345  mapdh8  37395  hdmap1l6d  37420  hdmap10  37449  hdmaprnlem17N  37472  hdmaplkr  37522  hdmapip0  37524  hgmapvv  37535  cmpfiiin  37577  pellexlem4  37713  pellqrex  37760  acongtr  37862  acongrep  37864  jm2.23  37880  rp-fakeanorass  38175  rp-isfinite6  38181  inintabss  38201  rfovcnvf1od  38615  clsk1indlem3  38658  ntrclsk13  38686  pm10.55  38885  refsum2cnlem1  39510  axccd2  39744  fmuldfeq  40133  climsuse  40158  limclner  40201  climxlim2lem  40389  icccncfext  40418  stoweidlem26  40561  stoweidlem52  40587  stoweidlem57  40592  fourierdlem20  40662  fourierdlem41  40683  fourierdlem52  40693  fourierdlem64  40705  fourierdlem102  40743  fourierdlem114  40755  ovolval4lem1  41184  preimagelt  41233  preimalegt  41234  afvelrn  41569  elfz2z  41650  2ffzoeq  41663  fargshiftfva  41704  ccatpfx  41734  pfxccat3  41751  pfxccatpfx2  41753  pfxccat3a  41754  reuccatpfxs1  41759  fmtnoprmfac1  41802  proththd  41856  opoeALTV  41919  evensumeven  41941  sbgoldbalt  41994  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  tgoldbach  42030  tgoldbachOLD  42037  uspgrsprfo  42081  assintop  42170  isringrng  42206  rnglz  42209  c0snmgmhm  42239  zrrnghm  42242  uzlidlring  42254  2zrngnmrid  42275  cznrng  42280  rnghmsubcsetclem2  42301  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  lmodvsmdi  42488  lincsum  42543  lincsumcl  42545  el0ldep  42580  ldepspr  42587  lindssnlvec  42600  modn0mul  42640  m1modmmod  42641  elbigolo1  42676  nn0digval  42719  setrec1lem3  42761  aacllem  42875
  Copyright terms: Public domain W3C validator