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

Theorem anim1i 616
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 614 1 ((𝜑𝜒) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  sylanl1  679  sylanr1  681  eu6im  2574  r19.28v  3187  rmob  3847  eqeuel  4323  preq12nebg  4821  fores  6767  ssimaex  6927  dffv2  6937  exfo  7056  fpropnf1  7215  oprabv  7418  ndmovass  7543  fun11uni  7870  fabexg  7872  f1oabexg  7874  f1iun  7877  soxp  8062  tz7.48lem  8388  tz7.49c  8393  omass  8528  oewordri  8540  omabs  8598  sbthlem9  9036  pssnn  9113  fineqvlem  9207  pssnnOLD  9210  domunfican  9265  fiint  9269  fsuppsssupp  9322  sup0  9403  inf1  9559  infeq5  9574  cantnfle  9608  rankuni  9800  djuunxp  9858  acndom  9988  acnnum  9989  cdainflem  10124  cfcof  10211  ac6num  10416  ac6s2  10423  brdom5  10466  brdom4  10467  genpnnp  10942  divmulasscom  11838  lediv2a  12050  supmul1  12125  infregelb  12140  nn2ge  12181  btwnz  12607  eluz2b2  12847  uz2mulcl  12852  eqreznegel  12860  xrsupexmnf  13225  xrinfmexpnf  13226  xrsupsslem  13227  xrinfmsslem  13228  supxrun  13236  ioo0  13290  elioo4g  13325  fz0fzelfz0  13548  fz0fzdiffz0  13551  2ffzeq  13563  elfzodifsumelfzo  13639  elfzom1elp1fzo  13640  zpnn0elfzo  13646  elfzom1elp1fzo1  13673  fzonfzoufzol  13676  quoremnn0  13762  zmodidfzoimp  13807  modabs  13810  modmuladd  13819  modifeq2int  13839  modaddmulmod  13844  expcl2lem  13980  hashgt23el  14325  hashreshashfun  14340  iswrdsymb  14420  ccatcl  14463  ccatsymb  14471  swrdfv2  14550  swrdsbslen  14553  swrdspsleq  14554  pfxswrd  14595  pfxccatin12lem3  14621  pfxccatpfx2  14626  swrdccat3blem  14628  reuccatpfxs1  14636  repswccat  14675  cshweqdifid  14709  lswco  14729  repsco  14730  s4f1o  14808  trclun  14900  mulre  15007  rediv  15017  imdiv  15024  resqrex  15136  caurcvg2  15563  fsumdifsnconst  15677  modfsummods  15679  tanval  16011  p1modz1  16144  negdvdsb  16156  muldvds1  16164  muldvds2  16165  dvdscmulr  16168  dvdsmulcr  16169  sumodd  16271  divalglem8  16283  divgcdnn  16396  lcmfunsnlem2lem2  16516  lcmfun  16522  2mulprm  16570  maxprmfct  16586  vfermltlALT  16675  modprm0  16678  pcpremul  16716  pcmul  16724  oddprmdvds  16776  prmdvdsprmo  16915  cshwsidrepsw  16967  gsumccat  18652  grpissubg  18949  gsmsymgreqlem2  19214  symgfixfo  19222  fsfnn0gsumfsffz  19761  irredn0  20133  gim0to0  20177  lsppratlem1  20611  cnfldfunALT  20812  dvdsrzring  20885  mpofrlmd  21186  matinvgcell  21787  mat1dimcrng  21829  dmatscmcl  21855  scmatscm  21865  scmatghm  21885  scmatmhm  21886  ma1repvcl  21922  slesolinv  22032  slesolinvbi  22033  cramerimplem1  22035  cramerimp  22038  cramerlem1  22039  cramer  22043  cpmatacl  22068  cpmatmcl  22071  mat2pmatghm  22082  mat2pmatmul  22083  m2pmfzgsumcl  22100  decpmatmul  22124  decpmatmulsumfsupp  22125  pmatcollpwfi  22134  pm2mpf1  22151  pm2mpghm  22168  pm2mpmhmlem1  22170  monmat2matmon  22176  chpdmatlem2  22191  chpdmat  22193  cpmadugsumlemB  22226  cpmadugsumlemC  22227  cpmadugsumlemF  22228  clscld  22401  neiptopnei  22486  2ndcdisj2  22811  comppfsc  22886  tx1stc  23004  opnfbas  23196  fbasfip  23222  alexsublem  23398  alexsubALTlem4  23404  cnextcn  23421  ngpocelbl  24071  cphipval  24610  bcthlem5  24695  vitalilem4  24978  vitalilem5  24979  itg2mulc  25115  bddiblnc  25209  dvcobr  25313  dvcnvlem  25343  dvferm1  25352  dvne0  25378  mdegmullem  25446  plyeq0lem  25574  plyexmo  25676  aalioulem5  25699  aalioulem6  25700  aaliou  25701  cxple2a  26057  cxpaddlelem  26107  cxpaddle  26108  relogbcxpb  26140  bcmono  26628  lgsprme0  26690  gausslemma2dlem0e  26711  gausslemma2dlem1a  26716  gausslemma2dlem6  26723  lgsquadlem2  26732  2lgsoddprm  26767  elno2  27005  cofcutr  27246  colinearalg  27862  axcontlem3  27918  umgrislfupgrlem  28076  edgupgr  28088  usgruspgrb  28135  usgrislfuspgr  28138  edgssv2  28149  umgr2edg  28160  uspgredg2v  28175  usgrexmplef  28210  subupgr  28238  subusgr  28240  nbupgrres  28315  nb3gr2nb  28335  nbupgruvtxres  28358  cusgrres  28399  cusgrsizeindslem  28402  cusgrsizeinds  28403  vtxdun  28432  finrusgrfusgr  28516  cusgrrusgr  28532  spthdep  28685  cycliscrct  28750  crctcshwlkn0lem6  28763  crctcshwlkn0lem7  28764  crctcshtrl  28771  crctcsh  28772  umgr2adedgwlkonALT  28895  elwwlks2  28914  elwspths2spth  28915  rusgrnumwwlk  28923  clwlkclwwlklem2a  28945  clwlkclwwlklem3  28948  clwwisshclwws  28962  wwlksubclwwlk  29005  eleclclwwlknlem2  29008  eupth2lem3lem3  29177  eucrct2eupth1  29191  frgr3v  29222  3vfriswmgr  29225  1to3vfriswmgr  29227  3cyclfrgr  29235  vdgn1frgrv2  29243  frgrwopreglem5  29268  frgrwopreglem5ALT  29269  frrusgrord0lem  29286  frrusgrord0  29287  2clwwlk2clwwlk  29297  extwwlkfab  29299  numclwwlk1lem2fo  29305  friendshipgt3  29345  ex-natded9.20-2  29365  grpoidinvlem3  29451  grpoidinv  29453  nmobndseqi  29724  nmobndseqiALT  29725  hvaddsub4  30023  ocsh  30228  5oalem2  30600  5oalem5  30603  3oalem2  30608  pjjsi  30645  hoadddir  30749  leopmul  31079  stge1i  31183  hatomistici  31307  mdsymlem2  31349  mdsymlem5  31352  addltmulALT  31391  isoun  31618  fsumiunle  31728  lsmsnorb  32175  crefdf  32432  qqhre  32604  esumiun  32696  sxbrsigalem0  32874  dya2iocnei  32885  sxbrsigalem5  32891  sibfinima  32942  eulerpartlemgs2  32983  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemsup  33107  bnj529  33356  bnj945  33388  bnj1098  33398  bnj1533  33467  bnj605  33522  bnj594  33527  bnj607  33531  bnj966  33559  bnj967  33560  bnj996  33571  bnj999  33573  bnj1006  33575  bnj1118  33599  bnj1172  33616  bnj1279  33633  bnj1296  33636  bnj1498  33676  fnrelpredd  33696  lfuhgr3  33716  loop1cycl  33734  cvmsi  33862  satf0op  33974  satffunlem1lem1  33999  satffunlem2lem1  34001  fv2ndcnv  34355  trisegint  34616  funtransport  34619  btwnconn1lem4  34678  btwnconn2  34690  segcon2  34693  outsideofeu  34719  isfne  34814  lukshef-ax2  34890  limsucncmpi  34920  bj-nsnid  35544  bj-restn0b  35565  bj-eldiag2  35651  bj-isrvec2  35774  pibt2  35891  unccur  36064  lindsadd  36074  lindsenlbs  36076  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem26  36107  poimirlem27  36108  poimirlem29  36110  poimirlem30  36111  poimirlem32  36113  heicant  36116  ismblfin  36122  itg2gt0cn  36136  areacirc  36174  opelopab3  36179  isdivrngo  36412  isdrngo2  36420  fldcrngo  36466  flddmn  36520  refrelredund4  37100  mainer2  37311  cmtbr4N  37720  linepsubN  38218  pmapsub  38234  paddasslem14  38299  pclcmpatN  38367  trlval2  38629  cdleme20  38790  cdleme21j  38802  dvalveclem  39491  dia2dimlem7  39536  dvhlveclem  39574  docaclN  39590  dihjat1  39895  mapdhcl  40193  mapdh6dN  40205  mapdh8  40254  hdmap1l6d  40279  hdmap10  40306  hdmaprnlem17N  40329  hdmaplkr  40379  hdmapip0  40381  hgmapvv  40392  cmpfiiin  41023  pellexlem4  41158  pellqrex  41205  acongtr  41305  acongrep  41307  jm2.23  41323  omlimcl2  41579  onsucf1lem  41607  oege1  41643  nnoeomeqom  41649  cantnfresb  41661  ofoafg  41671  ofoafo  41673  ofoaass  41677  ofoacom  41678  naddcnfass  41686  rp-fakeanorass  41792  rp-isfinite6  41797  harval3  41817  inintabss  41857  rfovcnvf1od  42283  clsk1indlem3  42322  ntrclsk13  42350  pm10.55  42656  refsum2cnlem1  43249  axccd2  43458  mptssid  43474  fmuldfeq  43831  climsuse  43856  limclner  43899  climxlim2lem  44093  icccncfext  44135  stoweidlem26  44274  stoweidlem52  44300  stoweidlem57  44305  fourierdlem20  44375  fourierdlem41  44396  fourierdlem52  44406  fourierdlem64  44418  fourierdlem102  44456  fourierdlem114  44468  ovolval4lem1  44897  preimagelt  44947  preimalegt  44948  funressneu  45288  afvelrn  45407  elfz2z  45554  2ffzoeq  45567  imasetpreimafvbijlemfv  45601  imasetpreimafvbijlemf1  45603  fargshiftfva  45642  ichreuopeq  45672  2exopprim  45724  reuopreuprim  45725  fmtnoprmfac1  45764  proththd  45813  opoeALTV  45882  evensumeven  45906  sbgoldbalt  45980  evengpop3  45997  evengpoap3  45998  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  wtgoldbnnsum4prm  46001  bgoldbnnsum3prm  46003  tgoldbach  46016  isomushgr  46025  assintop  46150  isringrng  46186  rnglz  46189  c0snmgmhm  46219  zrrnghm  46222  uzlidlring  46234  2zrngnmrid  46255  cznrng  46260  rnghmsubcsetclem2  46281  rhmsubcsetclem2  46327  rhmsubcrngclem2  46333  lmodvsmdi  46465  lincsum  46517  lincsumcl  46519  el0ldep  46554  ldepspr  46561  lindssnlvec  46574  modn0mul  46613  m1modmmod  46614  nn0digval  46693  1arympt1fv  46732  eenglngeehlnmlem1  46830  rrx2linest  46835  line2  46845  itsclc0yqe  46854  r19.41dv  46894  setrec1lem3  47141  aacllem  47255
  Copyright terms: Public domain W3C validator