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

Theorem sylan9eq 2675
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 2640 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 494 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614
This theorem is referenced by:  sylan9req  2676  sylan9eqr  2677  difeq12  3721  uneq12  3760  ineq12  3807  ssdifim  3860  ifeq12  4101  ifbi  4105  ifeq12da  4116  preq12  4268  prprc  4300  opeq12  4402  opthwiener  4974  xpeq12  5132  sosn  5186  nfimad  5473  coi2  5650  funprg  5938  funtpg  5940  funcnvtp  5949  funcnvqp  5950  funcnvqpOLD  5951  funimass1  5969  f1orescnv  6150  resdif  6155  fvmpt2  6289  fvmptnf  6300  fveqressseq  6353  oveq12  6656  cbvmpt2v  6732  ovmpt2g  6792  caofinvl  6921  eqopi  7199  el2mpt2csbcl  7247  fmpt2co  7257  mpt2sn  7265  supp0cosupp0  7331  mpt2curryd  7392  fvmpt2curryd  7394  wrecseq123  7405  rdgsucmptf  7521  frsucmpt  7530  oevn0  7592  oa0r  7615  om1r  7620  oe1m  7622  omass  7657  oeoalem  7673  oeoa  7674  oeoe  7676  map0g  7894  xpcomco  8047  sbthlem4  8070  sbthlem5  8071  xpmapenlem  8124  phplem3  8138  phplem4  8139  unxpdomlem3  8163  funsnfsupp  8296  ordtypelem7  8426  cardennn  8806  dfac9  8955  cdaassen  9001  alephsing  9095  axcc3  9257  ac6num  9298  konigthlem  9387  canthp1lem2  9472  ordpipq  9761  ltrnq  9798  addclprlem2  9836  mulclprlem  9838  prlem934  9852  prlem936  9866  mulcmpblnrlem  9888  addcnsr  9953  mulcnsr  9954  axcnre  9982  recex  10656  rpnnen1lem3  11813  rpnnen1lem5  11815  rpnnen1lem3OLD  11819  rpnnen1lem5OLD  11821  xaddpnf1  12054  xaddpnf2  12055  xaddmnf1  12056  xaddmnf2  12057  rexadd  12060  xnn0xaddcl  12063  xaddnemnf  12064  xaddnepnf  12065  xadddilem  12121  addmodlteq  12740  om2uzrani  12746  om2uzrdg  12750  seqf1olem2  12836  seqf1o  12837  modexp  12994  faclbnd4lem3  13077  hashunsng  13176  lsw1  13349  swrdfv  13418  swrdccat  13487  ccats1swrdeqbi  13492  revfv  13506  cshwsublen  13536  wrdlen2  13682  wrdl2exs2  13684  wwlktovf1  13694  relexp0  13757  relexpcnv  13769  shftcan1  13817  remul2  13864  immul2  13871  sumss  14449  geomulcvg  14601  fprodss  14672  binomfallfaclem2  14765  bpolylem  14773  ef0lem  14803  efieq1re  14923  rpnnen2lem1  14937  ruclem3  14956  dvdsnegb  14993  dvdscmul  15002  dvds2ln  15008  dvds2add  15009  dvds2sub  15010  gcdn0val  15214  rpmulgcd  15269  lcmn0val  15302  odzval  15490  pcval  15543  pcmpt  15590  prmreclem4  15617  1arithlem2  15622  vdwlem8  15686  ramcl2lem  15707  ramtcl  15708  ramtub  15710  ramcl2  15714  ramcl  15727  setsval  15882  prfcl  16837  curf1cl  16862  curfcl  16866  hofcl  16893  yonedalem4c  16911  psssdm  17210  grplactval  17511  cntzval  17748  f1omvdco2  17862  pmtrfinv  17875  psgnunilem5  17908  odlem2  17952  gexlem2  17991  lsmvalx  18048  efgtval  18130  efgredlema  18147  vrgpval  18174  cyggex  18293  gsumcom2  18368  dvdsrtr  18646  abvtrivd  18834  lmhmco  19037  reslmhm  19046  lvecinv  19107  mplmon2  19487  subrgasclcl  19493  coe1fv  19570  coe1fzgsumdlem  19665  evl1gsumdlem  19714  zrhmulg  19852  znzrhval  19889  ocvval  20005  mat1dimscm  20275  dmatid  20295  scmatdmat  20315  mavmul0g  20353  1marepvmarrepid  20375  mdetunilem2  20413  gsummatr01lem3  20457  gsummatr01  20459  smadiadetlem3  20468  m2cpminvid2lem  20553  chpdmatlem2  20638  isopn3  20864  cnpval  21034  ptbasfi  21378  dfac14  21415  cnmptkk  21480  xkofvcn  21481  cnmptk1p  21482  cnmptk2  21483  xkocnv  21611  flfval  21788  ptcmplem3  21852  ptcmpg  21855  tmdmulg  21890  prdsxmslem2  22328  subgnm2  22432  nmoval  22513  fsum2cn  22668  pcovalg  22806  isclmp  22891  cphnm  22987  tchnmval  23022  ovolctb  23252  ioorcl  23339  uniioombllem2  23345  itg1addlem3  23459  itg1climres  23475  itg2uba  23504  itg2splitlem  23509  elcpn  23691  dvexp  23710  dvexp2  23711  rolle  23747  cmvth  23748  mvth  23749  dvlip  23750  dvlipcn  23751  dvlip2  23752  dveq0  23757  dv11cn  23758  lhop1lem  23770  lhop2  23772  lhop  23773  dvcvx  23777  ftc2ditglem  23802  itgsubstlem  23805  ig1pval  23926  elply2  23946  coeid2  23989  coemul  24002  taylthlem2  24122  ulmdvlem1  24148  mtest  24152  pserval2  24159  abelthlem1  24179  abelthlem3  24181  abelthlem8  24187  abelthlem9  24188  pige3  24263  0cxp  24406  leibpi  24663  igamgam  24769  mule1  24868  bposlem5  25007  lgsval3  25034  lgsdinn0  25064  dchrvmasumlem1  25178  dchrisum0flblem1  25191  rpvmasum2  25195  padicval  25300  axsegconlem1  25791  ax5seglem9  25811  axpasch  25815  axeuclidlem  25836  axcontlem2  25839  finsumvtxdg2ssteplem4  26438  usgr2wlkspthlem2  26648  crctcshlem4  26706  wwlknp  26728  wlkiswwlks2lem3  26751  wwlksnred  26781  wwlksnextproplem2  26799  wspthsnwspthsnon  26805  umgrwwlks2on  26844  clwlkclwwlklem2a  26893  clwwlksf  26908  clwwlksext2edg  26916  wwlksext2clwwlk  26917  clwwisshclwwsn  26922  erclwwlksnsym  26940  erclwwlksntr  26941  eupth2lem3lem3  27083  eucrct2eupth  27098  fusgreghash2wspv  27186  numclwwlkovf2ex  27204  numclwlk1lem2f1  27211  grpoidinvlem4  27345  grpoinvval  27361  grpodivval  27373  ipval  27542  sspgval  27568  sspsval  27570  sspnval  27576  nmooval  27602  ipasslem1  27670  ipasslem4  27673  hial0  27943  hial02  27944  ocsh  28126  pjhval  28240  hosval  28583  homval  28584  hodval  28585  hfsval  28586  hfmval  28587  braval  28787  kbval  28797  eigvalval  28803  0hmop  28826  adj0  28837  lnopeq0i  28850  nmopcoi  28938  pjclem4  29042  pj3si  29050  hstoh  29075  strlem3a  29095  hstrlem3a  29103  mdexchi  29178  atcv0eq  29222  atcv1  29223  fpwrelmap  29493  smatfval  29846  measxun2  30258  measdivcstOLD  30272  measdivcst  30273  ddeval1  30282  ddeval0  30283  ballotlemfp1  30538  signswmnd  30619  signstfvneq0  30634  ftc2re  30661  itgexpif  30669  bnj1128  31043  subfacp1lem3  31149  subfacp1lem5  31151  cvmlift2lem3  31272  msubco  31413  altopthsn  32052  fnetr  32330  fnejoin2  32348  bj-evalid  33012  finxpreclem3  33210  finxpreclem5  33212  finxpreclem6  33213  curf  33367  curunc  33371  matunitlindf  33387  poimirlem4  33393  poimirlem25  33414  mblfinlem2  33427  mblfinlem3  33428  mbfresfi  33436  itg2addnclem  33441  itg2addnc  33444  ftc1anclem5  33469  isbnd3  33563  bndss  33565  grposnOLD  33661  ghomco  33670  lkrval  34201  pmapval  34869  polvalN  35017  watvalN  35105  ldilset  35221  ltrnset  35230  dilsetN  35266  trnsetN  35269  trlset  35274  trlval  35275  cdleme16b  35392  cdleme31fv1  35505  cdlemg1idlemN  35686  tgrpset  35859  tendoset  35873  erngset  35914  erngplus  35917  erngmul  35920  erngset-rN  35922  erngplus-rN  35925  dvaset  36119  dvaplusg  36123  dvamulr  36126  dvavadd  36129  dvavsca  36131  diafval  36146  dvhset  36196  dvhmulr  36201  dvhvadd  36207  dvhvsca  36216  docafvalN  36237  djafvalN  36249  dibfval  36256  dicfval  36290  dihfval  36346  dihval  36347  dihvalc  36348  dihvalb  36352  dochfval  36465  djhfval  36512  lcdval  36704  mapdfval  36742  mapdn0  36784  hvmapfval  36874  hdmap1fval  36912  hdmapfval  36945  hgmapfval  37004  pw2f1ocnv  37430  hbtlem7  37521  relexp0a  37834  ntrclscls00  38190  dvconstbi  38359  expgrowth  38360  addrfv  38499  subrfv  38500  mulvfv  38501  refsum2cnlem1  39022  limcperiod  39666  cncfiooiccre  39877  dvbdfbdioolem1  39912  itgioocnicc  39962  fourierdlem73  40165  fourierdlem82  40174  fourierdlem94  40186  fourierdlem103  40195  fourierdlem104  40196  fourierdlem113  40205  sqwvfoura  40214  etransclem46  40266  nnfoctbdjlem  40441  ovn0  40549  smflim  40754  afveu  41002  ccats1pfxeqbi  41202  lighneallem3  41295  mogoldbblem  41400  sbgoldbwt  41436  nnsum4primeseven  41459  nnsum4primesevenALTV  41460  bgoldbtbnd  41468  lmod0rng  41639  rnghmval  41662  lmodvsmdi  41934  lincdifsn  41984  lcoel0  41988  islindeps2  42043  blenn0  42138  nn0sumshdiglemA  42184  aacllem  42318
  Copyright terms: Public domain W3C validator