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

Theorem sylan9eq 2825
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1 (𝜑𝐴 = 𝐵)
sylan9eq.2 (𝜓𝐵 = 𝐶)
Assertion
Ref Expression
sylan9eq ((𝜑𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2 (𝜑𝐴 = 𝐵)
2 sylan9eq.2 . 2 (𝜓𝐵 = 𝐶)
3 eqtr 2790 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 583 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  sylan9req  2826  sylan9eqr  2827  difeq12  3874  uneq12  3913  ineq12  3960  ssdifim  4011  ifeq12  4242  ifbi  4246  ifeq12da  4257  preq12  4406  prprc  4438  opeq12  4541  opthwiener  5107  opthhausdorff0  5111  xpeq12  5274  sosn  5328  nfimad  5616  coi2  5796  funprg  6083  funtpg  6084  funcnvtp  6092  funcnvqp  6093  funimass1  6111  f1orescnv  6293  resdif  6298  fvmpt2  6433  fvmptnf  6444  fveqressseq  6498  oveq12  6802  cbvmpt2v  6882  ovmpt2g  6942  caofinvl  7071  eqopi  7351  el2mpt2csbcl  7400  fmpt2co  7411  mpt2sn  7419  supp0cosupp0  7486  mpt2curryd  7547  fvmpt2curryd  7549  wrecseq123  7560  rdgsucmptf  7677  frsucmpt  7686  oevn0  7749  oa0r  7772  om1r  7777  oe1m  7779  omass  7814  oeoalem  7830  oeoa  7831  oeoe  7833  map0g  8050  xpcomco  8206  sbthlem4  8229  sbthlem5  8230  xpmapenlem  8283  phplem3  8297  phplem4  8298  unxpdomlem3  8322  funsnfsupp  8455  ordtypelem7  8585  cardennn  9009  dfac9  9160  cdaassen  9206  alephsing  9300  axcc3  9462  ac6num  9503  konigthlem  9592  canthp1lem2  9677  ordpipq  9966  ltrnq  10003  addclprlem2  10041  mulclprlem  10043  prlem934  10057  prlem936  10071  mulcmpblnrlem  10093  addcnsr  10158  mulcnsr  10159  axcnre  10187  recex  10861  rpnnen1lem3  12019  rpnnen1lem5  12021  rpnnen1lem3OLD  12025  rpnnen1lem5OLD  12027  xaddpnf1  12262  xaddpnf2  12263  xaddmnf1  12264  xaddmnf2  12265  rexadd  12268  xnn0xaddcl  12271  xaddnemnf  12272  xaddnepnf  12273  xadddilem  12329  addmodlteq  12953  om2uzrani  12959  om2uzrdg  12963  seqf1olem2  13048  seqf1o  13049  modexp  13206  faclbnd4lem3  13286  hashunsng  13383  lsw1  13551  swrdfv  13632  swrdccat  13702  ccats1swrdeqbi  13707  revfv  13721  cshwsublen  13751  wrdlen2  13898  wrdl2exs2  13900  wwlktovf1  13910  relexp0  13971  relexpcnv  13983  shftcan1  14031  remul2  14078  immul2  14085  sumss  14663  geomulcvg  14814  fprodss  14885  binomfallfaclem2  14977  bpolylem  14985  ef0lem  15015  efieq1re  15135  rpnnen2lem1  15149  ruclem3  15168  dvdsnegb  15208  dvdscmul  15217  dvds2ln  15223  dvds2add  15224  dvds2sub  15225  gcdn0val  15428  rpmulgcd  15483  lcmn0val  15516  odzval  15703  pcval  15756  pcmpt  15803  prmreclem4  15830  1arithlem2  15835  vdwlem8  15899  ramcl2lem  15920  ramtcl  15921  ramtub  15923  ramcl2  15927  ramcl  15940  setsval  16095  prfcl  17051  curf1cl  17076  curfcl  17080  hofcl  17107  yonedalem4c  17125  psssdm  17424  grplactval  17725  cntzval  17961  f1omvdco2  18075  pmtrfinv  18088  psgnunilem5  18121  odlem2  18165  gexlem2  18204  lsmvalx  18261  efgtval  18343  efgredlema  18360  vrgpval  18387  cyggex  18506  gsumcom2  18581  dvdsrtr  18860  abvtrivd  19050  lmhmco  19256  reslmhm  19265  lvecinv  19326  mplmon2  19708  subrgasclcl  19714  coe1fv  19791  coe1fzgsumdlem  19886  evl1gsumdlem  19935  zrhmulg  20073  znzrhval  20110  ocvval  20228  mat1dimscm  20499  dmatid  20519  scmatdmat  20539  mavmul0g  20577  1marepvmarrepid  20599  mdetunilem2  20637  gsummatr01lem3  20682  gsummatr01  20684  smadiadetlem3  20693  m2cpminvid2lem  20779  chpdmatlem2  20864  isopn3  21091  cnpval  21261  ptbasfi  21605  dfac14  21642  cnmptkk  21707  xkofvcn  21708  cnmptk1p  21709  cnmptk2  21710  xkocnv  21838  flfval  22014  ptcmplem3  22078  ptcmpg  22081  tmdmulg  22116  prdsxmslem2  22554  subgnm2  22658  nmoval  22739  fsum2cn  22894  pcovalg  23031  isclmp  23116  cphnm  23212  tchnmval  23247  ovolctb  23478  ioorcl  23565  uniioombllem2  23571  itg1addlem3  23685  itg1climres  23701  itg2uba  23730  itg2splitlem  23735  elcpn  23917  dvexp  23936  dvexp2  23937  rolle  23973  cmvth  23974  mvth  23975  dvlip  23976  dvlipcn  23977  dvlip2  23978  dveq0  23983  dv11cn  23984  lhop1lem  23996  lhop2  23998  lhop  23999  dvcvx  24003  ftc2ditglem  24028  itgsubstlem  24031  ig1pval  24152  elply2  24172  coeid2  24215  coemul  24228  taylthlem2  24348  ulmdvlem1  24374  mtest  24378  pserval2  24385  abelthlem1  24405  abelthlem3  24407  abelthlem8  24413  abelthlem9  24414  pige3  24490  0cxp  24633  leibpi  24890  igamgam  24996  mule1  25095  bposlem5  25234  lgsval3  25261  lgsdinn0  25291  dchrvmasumlem1  25405  dchrisum0flblem1  25418  rpvmasum2  25422  padicval  25527  axsegconlem1  26018  ax5seglem9  26038  axpasch  26042  axeuclidlem  26063  axcontlem2  26066  finsumvtxdg2ssteplem4  26679  usgr2wlkspthlem2  26889  crctcshlem4  26948  wwlknp  26971  wlkiswwlks2lem3  27005  wwlksnred  27036  wwlksnextproplem2  27055  wspthsnwspthsnonOLD  27063  umgrwwlks2on  27105  clwlkclwwlklem2a  27148  clwwisshclwwsn  27166  clwwlknlbonbgr1  27195  clwwlkn1loopb  27199  clwwlkf  27203  clwwlkext2edg  27213  wwlksext2clwwlkOLD  27215  erclwwlknsym  27228  erclwwlkntr  27229  clwwlknon1  27272  clwwlknonex2  27285  eupth2lem3lem3  27410  eucrct2eupth  27425  fusgreghash2wspv  27517  2clwwlk2clwwlklem  27530  2clwwlk2clwwlk  27534  numclwwlk1lem2f1  27543  grpoidinvlem4  27701  grpoinvval  27717  grpodivval  27729  ipval  27898  sspgval  27924  sspsval  27926  sspnval  27932  nmooval  27958  ipasslem1  28026  ipasslem4  28029  hial0  28299  hial02  28300  ocsh  28482  pjhval  28596  hosval  28939  homval  28940  hodval  28941  hfsval  28942  hfmval  28943  braval  29143  kbval  29153  eigvalval  29159  0hmop  29182  adj0  29193  lnopeq0i  29206  nmopcoi  29294  pjclem4  29398  pj3si  29406  hstoh  29431  strlem3a  29451  hstrlem3a  29459  mdexchi  29534  atcv0eq  29578  atcv1  29579  fpwrelmap  29848  smatfval  30201  measxun2  30613  measdivcstOLD  30627  measdivcst  30628  ddeval1  30637  ddeval0  30638  ballotlemfp1  30893  signswmnd  30974  signstfvneq0  30989  ftc2re  31016  itgexpif  31024  bnj1128  31396  subfacp1lem3  31502  subfacp1lem5  31504  cvmlift2lem3  31625  msubco  31766  altopthsn  32405  fnetr  32683  fnejoin2  32701  bj-evalid  33360  finxpreclem3  33567  finxpreclem5  33569  finxpreclem6  33570  curf  33720  curunc  33724  matunitlindf  33740  poimirlem4  33746  poimirlem25  33767  mblfinlem2  33780  mblfinlem3  33781  mbfresfi  33788  itg2addnclem  33793  itg2addnc  33796  ftc1anclem5  33821  isbnd3  33915  bndss  33917  grposnOLD  34013  ghomco  34022  qseq12  34401  xrneq12  34487  lkrval  34897  pmapval  35565  polvalN  35713  watvalN  35801  ldilset  35917  ltrnset  35926  dilsetN  35962  trnsetN  35965  trlset  35970  trlval  35971  cdleme16b  36088  cdleme31fv1  36200  cdlemg1idlemN  36381  tgrpset  36554  tendoset  36568  erngset  36609  erngplus  36612  erngmul  36615  erngset-rN  36617  erngplus-rN  36620  dvaset  36814  dvaplusg  36818  dvamulr  36821  dvavadd  36824  dvavsca  36826  diafval  36841  dvhset  36891  dvhmulr  36896  dvhvadd  36902  dvhvsca  36911  docafvalN  36932  djafvalN  36944  dibfval  36951  dicfval  36985  dihfval  37041  dihval  37042  dihvalc  37043  dihvalb  37047  dochfval  37160  djhfval  37207  lcdval  37399  mapdfval  37437  mapdn0  37479  hvmapfval  37569  hdmap1fval  37606  hdmapfval  37637  hgmapfval  37696  pw2f1ocnv  38130  hbtlem7  38221  relexp0a  38534  ntrclscls00  38890  dvconstbi  39059  expgrowth  39060  addrfv  39198  subrfv  39199  mulvfv  39200  refsum2cnlem1  39718  limcperiod  40378  cncfiooiccre  40626  dvbdfbdioolem1  40661  itgioocnicc  40710  fourierdlem73  40913  fourierdlem82  40922  fourierdlem94  40934  fourierdlem103  40943  fourierdlem104  40944  fourierdlem113  40953  sqwvfoura  40962  etransclem46  41014  nnfoctbdjlem  41189  ovn0  41300  smflim  41505  afveu  41753  fvmptrabdm  41835  ccats1pfxeqbi  41959  lighneallem3  42052  mogoldbblem  42157  sbgoldbwt  42193  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  bgoldbtbnd  42225  lmod0rng  42396  rnghmval  42419  lmodvsmdi  42691  lincdifsn  42741  lcoel0  42745  islindeps2  42800  blenn0  42895  nn0sumshdiglemA  42941  aacllem  43078
  Copyright terms: Public domain W3C validator