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

Theorem anim1i 614
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 612 1 ((𝜑𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  sylanl1  676  sylanr1  678  eu6im  2653  r19.28v  3183  rmob  3871  eqeuel  4319  preq12nebg  4785  fores  6593  ssimaex  6741  dffv2  6749  exfo  6863  fpropnf1  7016  oprabv  7203  ndmovass  7325  fun11uni  7626  fabexg  7628  f1oabexg  7631  f1iun  7634  soxp  7812  tz7.48lem  8066  tz7.49c  8071  omass  8195  oewordri  8207  omabs  8263  sbthlem9  8623  fineqvlem  8720  pssnn  8724  domunfican  8779  fiint  8783  fsuppsssupp  8837  sup0  8918  inf1  9073  infeq5  9088  cantnfle  9122  rankuni  9280  djuunxp  9338  acndom  9465  acnnum  9466  cdainflem  9601  cfcof  9684  ac6num  9889  ac6s2  9896  brdom5  9939  brdom4  9940  genpnnp  10415  divmulasscom  11310  lediv2a  11522  supmul1  11598  infregelb  11613  nn2ge  11652  btwnz  12072  eluz2b2  12309  uz2mulcl  12314  eqreznegel  12322  xrsupexmnf  12686  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  supxrun  12697  ioo0  12751  elioo4g  12785  fz0fzelfz0  13001  fz0fzdiffz0  13004  2ffzeq  13016  elfzodifsumelfzo  13091  elfzom1elp1fzo  13092  zpnn0elfzo  13098  elfzom1elp1fzo1  13125  fzonfzoufzol  13128  quoremnn0  13212  zmodidfzoimp  13257  modabs  13260  modmuladd  13269  modifeq2int  13289  modaddmulmod  13294  expcl2lem  13429  hashgt23el  13773  hashreshashfun  13788  iswrdsymb  13869  ccatcl  13914  ccatsymb  13924  swrdfv2  14011  swrdsbslen  14014  swrdspsleq  14015  pfxswrd  14056  pfxccatin12lem3  14082  pfxccatpfx2  14087  swrdccat3blem  14089  reuccatpfxs1  14097  repswccat  14136  cshweqdifid  14170  lswco  14189  repsco  14190  s4f1o  14268  ccat2s1fvwALTOLD  14307  trclun  14362  mulre  14468  rediv  14478  imdiv  14485  resqrex  14598  caurcvg2  15022  fsumdifsnconst  15134  modfsummods  15136  tanval  15469  p1modz1  15602  negdvdsb  15614  muldvds1  15622  muldvds2  15623  dvdscmulr  15626  dvdsmulcr  15627  sumodd  15727  divalglem8  15739  divgcdnn  15851  lcmfunsnlem2lem2  15971  lcmfun  15977  2mulprm  16025  maxprmfct  16041  vfermltlALT  16127  modprm0  16130  pcpremul  16168  pcmul  16176  oddprmdvds  16227  prmdvdsprmo  16366  cshwsidrepsw  16415  gsumccat  17994  grpissubg  18237  gsmsymgreqlem2  18488  symgfixfo  18496  fsfnn0gsumfsffz  19032  irredn0  19382  gim0to0  19424  rim0to0OLD  19425  lsppratlem1  19848  dvdsrzring  20558  mpofrlmd  20849  matinvgcell  20972  mat1dimcrng  21014  dmatscmcl  21040  scmatscm  21050  scmatghm  21070  scmatmhm  21071  ma1repvcl  21107  slesolinv  21217  slesolinvbi  21218  cramerimplem1  21220  cramerimp  21223  cramerlem1  21224  cramer  21228  cpmatacl  21252  cpmatmcl  21255  mat2pmatghm  21266  mat2pmatmul  21267  m2pmfzgsumcl  21284  decpmatmul  21308  decpmatmulsumfsupp  21309  pmatcollpwfi  21318  pm2mpf1  21335  pm2mpghm  21352  pm2mpmhmlem1  21354  monmat2matmon  21360  chpdmatlem2  21375  chpdmat  21377  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  clscld  21583  neiptopnei  21668  2ndcdisj2  21993  comppfsc  22068  tx1stc  22186  opnfbas  22378  fbasfip  22404  alexsublem  22580  alexsubALTlem4  22586  cnextcn  22603  ngpocelbl  23240  cphipval  23773  bcthlem5  23858  vitalilem4  24139  vitalilem5  24140  itg2mulc  24275  dvcobr  24470  dvcnvlem  24500  dvferm1  24509  dvne0  24535  mdegmullem  24599  plyeq0lem  24727  plyexmo  24829  aalioulem5  24852  aalioulem6  24853  aaliou  24854  cxple2a  25209  cxpaddlelem  25259  cxpaddle  25260  relogbcxpb  25292  bcmono  25780  lgsprme0  25842  gausslemma2dlem0e  25863  gausslemma2dlem1a  25868  gausslemma2dlem6  25875  lgsquadlem2  25884  2lgsoddprm  25919  colinearalg  26623  axcontlem3  26679  umgrislfupgrlem  26834  edgupgr  26846  usgruspgrb  26893  usgrislfuspgr  26896  edgssv2  26907  umgr2edg  26918  uspgredg2v  26933  usgrexmplef  26968  subupgr  26996  subusgr  26998  nbupgrres  27073  nb3gr2nb  27093  nbupgruvtxres  27116  cusgrres  27157  cusgrsizeindslem  27160  cusgrsizeinds  27161  vtxdun  27190  finrusgrfusgr  27274  cusgrrusgr  27290  spthdep  27442  cycliscrct  27507  crctcshwlkn0lem6  27520  crctcshwlkn0lem7  27521  crctcshtrl  27528  crctcsh  27529  umgr2adedgwlkonALT  27653  elwwlks2  27672  elwspths2spth  27673  rusgrnumwwlk  27681  clwlkclwwlklem2a  27703  clwlkclwwlklem3  27706  clwwisshclwws  27720  wwlksubclwwlk  27764  eleclclwwlknlem2  27767  eupth2lem3lem3  27936  eucrct2eupth1  27950  frgr3v  27981  3vfriswmgr  27984  1to3vfriswmgr  27986  3cyclfrgr  27994  vdgn1frgrv2  28002  frgrwopreglem5  28027  frgrwopreglem5ALT  28028  frrusgrord0lem  28045  frrusgrord0  28046  2clwwlk2clwwlk  28056  extwwlkfab  28058  numclwwlk1lem2fo  28064  friendshipgt3  28104  ex-natded9.20-2  28124  grpoidinvlem3  28210  grpoidinv  28212  nmobndseqi  28483  nmobndseqiALT  28484  hvaddsub4  28782  ocsh  28987  5oalem2  29359  5oalem5  29362  3oalem2  29367  pjjsi  29404  hoadddir  29508  leopmul  29838  stge1i  29942  hatomistici  30066  mdsymlem2  30108  mdsymlem5  30111  addltmulALT  30150  isoun  30363  fsumiunle  30472  crefdf  31011  qqhre  31160  esumiun  31252  sxbrsigalem0  31428  dya2iocnei  31439  sxbrsigalem5  31445  sibfinima  31496  eulerpartlemgs2  31537  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemsup  31661  bnj529  31911  bnj945  31944  bnj1098  31954  bnj1533  32023  bnj605  32078  bnj594  32083  bnj607  32087  bnj966  32115  bnj967  32116  bnj996  32126  bnj999  32128  bnj1006  32130  bnj1118  32153  bnj1172  32170  bnj1279  32187  bnj1296  32190  bnj1498  32230  lfuhgr3  32263  loop1cycl  32281  cvmsi  32409  satf0op  32521  satffunlem1lem1  32546  satffunlem2lem1  32548  fv2ndcnv  32918  elno2  33058  trisegint  33386  funtransport  33389  btwnconn1lem4  33448  btwnconn2  33460  segcon2  33463  outsideofeu  33489  isfne  33584  lukshef-ax2  33660  limsucncmpi  33690  bj-nsnid  34256  bj-restn0b  34276  bj-eldiag2  34361  bj-isrvec2  34469  pibt2  34580  unccur  34756  lindsadd  34766  lindsenlbs  34768  matunitlindflem1  34769  matunitlindflem2  34770  poimirlem26  34799  poimirlem27  34800  poimirlem29  34802  poimirlem30  34803  poimirlem32  34805  heicant  34808  ismblfin  34814  itg2gt0cn  34828  bddiblnc  34843  areacirc  34868  opelopab3  34873  isdivrngo  35109  isdrngo2  35117  fldcrng  35163  flddmn  35217  refrelredund4  35750  cmtbr4N  36271  linepsubN  36768  pmapsub  36784  paddasslem14  36849  pclcmpatN  36917  trlval2  37179  cdleme20  37340  cdleme21j  37352  dvalveclem  38041  dia2dimlem7  38086  dvhlveclem  38124  docaclN  38140  dihjat1  38445  mapdhcl  38743  mapdh6dN  38755  mapdh8  38804  hdmap1l6d  38829  hdmap10  38856  hdmaprnlem17N  38879  hdmaplkr  38929  hdmapip0  38931  hgmapvv  38942  cmpfiiin  39172  pellexlem4  39307  pellqrex  39354  acongtr  39453  acongrep  39455  jm2.23  39471  rp-fakeanorass  39757  rp-isfinite6  39762  harval3  39782  inintabss  39816  rfovcnvf1od  40228  clsk1indlem3  40271  ntrclsk13  40299  pm10.55  40578  refsum2cnlem1  41171  axccd2  41372  mptssid  41387  fmuldfeq  41740  climsuse  41765  limclner  41808  climxlim2lem  42002  icccncfext  42046  stoweidlem26  42188  stoweidlem52  42214  stoweidlem57  42219  fourierdlem20  42289  fourierdlem41  42310  fourierdlem52  42320  fourierdlem64  42332  fourierdlem102  42370  fourierdlem114  42382  ovolval4lem1  42808  preimagelt  42857  preimalegt  42858  funressneu  43159  afvelrn  43244  elfz2z  43392  2ffzoeq  43405  imasetpreimafvbijlemfv  43439  imasetpreimafvbijlemf1  43441  fargshiftfva  43480  ichreuopeq  43512  2exopprim  43564  reuopreuprim  43565  fmtnoprmfac1  43604  proththd  43656  opoeALTV  43725  evensumeven  43749  sbgoldbalt  43823  evengpop3  43840  evengpoap3  43841  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  tgoldbach  43859  isomushgr  43868  uspgrsprfo  43900  assintop  44044  isringrng  44080  rnglz  44083  c0snmgmhm  44113  zrrnghm  44116  uzlidlring  44128  2zrngnmrid  44149  cznrng  44154  rnghmsubcsetclem2  44175  rhmsubcsetclem2  44221  rhmsubcrngclem2  44227  lmodvsmdi  44358  lincsum  44412  lincsumcl  44414  el0ldep  44449  ldepspr  44456  lindssnlvec  44469  modn0mul  44508  m1modmmod  44509  nn0digval  44588  eenglngeehlnmlem1  44652  rrx2linest  44657  line2  44667  itsclc0yqe  44676  setrec1lem3  44720  aacllem  44830
  Copyright terms: Public domain W3C validator