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

Theorem sylan9eq 2705
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 2670 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 493 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  sylan9req  2706  sylan9eqr  2707  difeq12  3756  uneq12  3795  ineq12  3842  ssdifim  3895  ifeq12  4136  ifbi  4140  ifeq12da  4151  preq12  4302  prprc  4334  opeq12  4435  opthwiener  5005  xpeq12  5168  sosn  5222  nfimad  5510  coi2  5690  funprg  5978  funtpg  5980  funcnvtp  5989  funcnvqp  5990  funcnvqpOLD  5991  funimass1  6009  f1orescnv  6190  resdif  6195  fvmpt2  6330  fvmptnf  6341  fveqressseq  6395  oveq12  6699  cbvmpt2v  6777  ovmpt2g  6837  caofinvl  6966  eqopi  7246  el2mpt2csbcl  7295  fmpt2co  7305  mpt2sn  7313  supp0cosupp0  7379  mpt2curryd  7440  fvmpt2curryd  7442  wrecseq123  7453  rdgsucmptf  7569  frsucmpt  7578  oevn0  7640  oa0r  7663  om1r  7668  oe1m  7670  omass  7705  oeoalem  7721  oeoa  7722  oeoe  7724  map0g  7939  xpcomco  8091  sbthlem4  8114  sbthlem5  8115  xpmapenlem  8168  phplem3  8182  phplem4  8183  unxpdomlem3  8207  funsnfsupp  8340  ordtypelem7  8470  cardennn  8847  dfac9  8996  cdaassen  9042  alephsing  9136  axcc3  9298  ac6num  9339  konigthlem  9428  canthp1lem2  9513  ordpipq  9802  ltrnq  9839  addclprlem2  9877  mulclprlem  9879  prlem934  9893  prlem936  9907  mulcmpblnrlem  9929  addcnsr  9994  mulcnsr  9995  axcnre  10023  recex  10697  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  xaddpnf1  12095  xaddpnf2  12096  xaddmnf1  12097  xaddmnf2  12098  rexadd  12101  xnn0xaddcl  12104  xaddnemnf  12105  xaddnepnf  12106  xadddilem  12162  addmodlteq  12785  om2uzrani  12791  om2uzrdg  12795  seqf1olem2  12881  seqf1o  12882  modexp  13039  faclbnd4lem3  13122  hashunsng  13219  lsw1  13387  swrdfv  13469  swrdccat  13539  ccats1swrdeqbi  13544  revfv  13558  cshwsublen  13588  wrdlen2  13734  wrdl2exs2  13736  wwlktovf1  13746  relexp0  13807  relexpcnv  13819  shftcan1  13867  remul2  13914  immul2  13921  sumss  14499  geomulcvg  14651  fprodss  14722  binomfallfaclem2  14815  bpolylem  14823  ef0lem  14853  efieq1re  14973  rpnnen2lem1  14987  ruclem3  15006  dvdsnegb  15046  dvdscmul  15055  dvds2ln  15061  dvds2add  15062  dvds2sub  15063  gcdn0val  15267  rpmulgcd  15322  lcmn0val  15355  odzval  15543  pcval  15596  pcmpt  15643  prmreclem4  15670  1arithlem2  15675  vdwlem8  15739  ramcl2lem  15760  ramtcl  15761  ramtub  15763  ramcl2  15767  ramcl  15780  setsval  15935  prfcl  16890  curf1cl  16915  curfcl  16919  hofcl  16946  yonedalem4c  16964  psssdm  17263  grplactval  17564  cntzval  17800  f1omvdco2  17914  pmtrfinv  17927  psgnunilem5  17960  odlem2  18004  gexlem2  18043  lsmvalx  18100  efgtval  18182  efgredlema  18199  vrgpval  18226  cyggex  18345  gsumcom2  18420  dvdsrtr  18698  abvtrivd  18888  lmhmco  19091  reslmhm  19100  lvecinv  19161  mplmon2  19541  subrgasclcl  19547  coe1fv  19624  coe1fzgsumdlem  19719  evl1gsumdlem  19768  zrhmulg  19906  znzrhval  19943  ocvval  20059  mat1dimscm  20329  dmatid  20349  scmatdmat  20369  mavmul0g  20407  1marepvmarrepid  20429  mdetunilem2  20467  gsummatr01lem3  20511  gsummatr01  20513  smadiadetlem3  20522  m2cpminvid2lem  20607  chpdmatlem2  20692  isopn3  20918  cnpval  21088  ptbasfi  21432  dfac14  21469  cnmptkk  21534  xkofvcn  21535  cnmptk1p  21536  cnmptk2  21537  xkocnv  21665  flfval  21841  ptcmplem3  21905  ptcmpg  21908  tmdmulg  21943  prdsxmslem2  22381  subgnm2  22485  nmoval  22566  fsum2cn  22721  pcovalg  22858  isclmp  22943  cphnm  23039  tchnmval  23074  ovolctb  23304  ioorcl  23391  uniioombllem2  23397  itg1addlem3  23510  itg1climres  23526  itg2uba  23555  itg2splitlem  23560  elcpn  23742  dvexp  23761  dvexp2  23762  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvlipcn  23802  dvlip2  23803  dveq0  23808  dv11cn  23809  lhop1lem  23821  lhop2  23823  lhop  23824  dvcvx  23828  ftc2ditglem  23853  itgsubstlem  23856  ig1pval  23977  elply2  23997  coeid2  24040  coemul  24053  taylthlem2  24173  ulmdvlem1  24199  mtest  24203  pserval2  24210  abelthlem1  24230  abelthlem3  24232  abelthlem8  24238  abelthlem9  24239  pige3  24314  0cxp  24457  leibpi  24714  igamgam  24820  mule1  24919  bposlem5  25058  lgsval3  25085  lgsdinn0  25115  dchrvmasumlem1  25229  dchrisum0flblem1  25242  rpvmasum2  25246  padicval  25351  axsegconlem1  25842  ax5seglem9  25862  axpasch  25866  axeuclidlem  25887  axcontlem2  25890  finsumvtxdg2ssteplem4  26500  usgr2wlkspthlem2  26710  crctcshlem4  26768  wwlknp  26791  wlkiswwlks2lem3  26825  wwlksnred  26855  wwlksnextproplem2  26873  wspthsnwspthsnonOLD  26881  umgrwwlks2on  26923  clwlkclwwlklem2a  26964  clwwisshclwwsn  26973  clwwlknlbonbgr1  27002  clwwlkn1loopb  27006  clwwlkf  27010  clwwlkext2edg  27020  wwlksext2clwwlkOLD  27022  erclwwlknsym  27034  erclwwlkntr  27035  clwwlknon1  27072  clwwlknonex2  27084  eupth2lem3lem3  27208  eucrct2eupth  27223  fusgreghash2wspv  27315  2clwwlk2clwwlklem2lem2  27329  2clwwlk2clwwlklem2  27330  2clwwlk2clwwlk  27338  numclwlk1lem2f1  27347  grpoidinvlem4  27489  grpoinvval  27505  grpodivval  27517  ipval  27686  sspgval  27712  sspsval  27714  sspnval  27720  nmooval  27746  ipasslem1  27814  ipasslem4  27817  hial0  28087  hial02  28088  ocsh  28270  pjhval  28384  hosval  28727  homval  28728  hodval  28729  hfsval  28730  hfmval  28731  braval  28931  kbval  28941  eigvalval  28947  0hmop  28970  adj0  28981  lnopeq0i  28994  nmopcoi  29082  pjclem4  29186  pj3si  29194  hstoh  29219  strlem3a  29239  hstrlem3a  29247  mdexchi  29322  atcv0eq  29366  atcv1  29367  fpwrelmap  29636  smatfval  29989  measxun2  30401  measdivcstOLD  30415  measdivcst  30416  ddeval1  30425  ddeval0  30426  ballotlemfp1  30681  signswmnd  30762  signstfvneq0  30777  ftc2re  30804  itgexpif  30812  bnj1128  31184  subfacp1lem3  31290  subfacp1lem5  31292  cvmlift2lem3  31413  msubco  31554  altopthsn  32193  fnetr  32471  fnejoin2  32489  bj-evalid  33153  finxpreclem3  33360  finxpreclem5  33362  finxpreclem6  33363  curf  33517  curunc  33521  matunitlindf  33537  poimirlem4  33543  poimirlem25  33564  mblfinlem2  33577  mblfinlem3  33578  mbfresfi  33586  itg2addnclem  33591  itg2addnc  33594  ftc1anclem5  33619  isbnd3  33713  bndss  33715  grposnOLD  33811  ghomco  33820  qseq12  34199  xrneq12  34285  lkrval  34693  pmapval  35361  polvalN  35509  watvalN  35597  ldilset  35713  ltrnset  35722  dilsetN  35758  trnsetN  35761  trlset  35766  trlval  35767  cdleme16b  35884  cdleme31fv1  35996  cdlemg1idlemN  36177  tgrpset  36350  tendoset  36364  erngset  36405  erngplus  36408  erngmul  36411  erngset-rN  36413  erngplus-rN  36416  dvaset  36610  dvaplusg  36614  dvamulr  36617  dvavadd  36620  dvavsca  36622  diafval  36637  dvhset  36687  dvhmulr  36692  dvhvadd  36698  dvhvsca  36707  docafvalN  36728  djafvalN  36740  dibfval  36747  dicfval  36781  dihfval  36837  dihval  36838  dihvalc  36839  dihvalb  36843  dochfval  36956  djhfval  37003  lcdval  37195  mapdfval  37233  mapdn0  37275  hvmapfval  37365  hdmap1fval  37403  hdmapfval  37436  hgmapfval  37495  pw2f1ocnv  37921  hbtlem7  38012  relexp0a  38325  ntrclscls00  38681  dvconstbi  38850  expgrowth  38851  addrfv  38990  subrfv  38991  mulvfv  38992  refsum2cnlem1  39510  limcperiod  40178  cncfiooiccre  40426  dvbdfbdioolem1  40461  itgioocnicc  40511  fourierdlem73  40714  fourierdlem82  40723  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  sqwvfoura  40763  etransclem46  40815  nnfoctbdjlem  40990  ovn0  41101  smflim  41306  afveu  41554  fvmptrabdm  41632  ccats1pfxeqbi  41756  lighneallem3  41849  mogoldbblem  41954  sbgoldbwt  41990  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbnd  42022  lmod0rng  42193  rnghmval  42216  lmodvsmdi  42488  lincdifsn  42538  lcoel0  42542  islindeps2  42597  blenn0  42692  nn0sumshdiglemA  42738  aacllem  42875
  Copyright terms: Public domain W3C validator