Theorem syl5eq 1940

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
syl5eq.1	|- (ph -> A = B)
syl5eq.2	|- C = A

Assertion

Ref	Expression
syl5eq	|- (ph -> C = B)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.2	. . 3 |- C = A
2	1	a1i 8	. 2 |- (ph -> C = A)
3		syl5eq.1	. 2 |- (ph -> A = B)
4	2, 3	eqtrd 1925	1 |- (ph -> C = B)

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  syl5req 1941  syl5eqr 1942  3eqtr4g 1953  abidhb 2423  csbconstgf 2551  csbvarg 2564  csbiegft 2573  csbabgOLD 2589  rabbirdv 2801  ssinOLD 2815  uneqin 2845  uneqinOLD 2846  disjssun 2932  prprc2 3109  difsnid 3131  opprc1 3170  sucprc 3740  orduniss2 3913  relop 4113  dmxp 4177  resabs1 4244  resabs2 4245  resopab2 4256  imasng 4287  ndmima 4300  xpdisj1 4337  xpdisj2 4338  resdisj 4340  resdisjOLD 4341  rnxp 4342  dfco2a 4394  unixp 4422  funtp 4468  fnun 4520  fnresdisj 4523  fnima 4530  fcoi1 4584  f1orescnv 4655  resdif 4659  fvprc 4678  fnrnfv 4718  fvopab4gf 4744  fvopabn 4749  fvopabgf 4750  fvopabnf 4751  fvopab6 4757  fvsnun2 4765  elrnopabg 4773  fopab2 4796  rnssopab 4798  fopabco 4805  funiunfv 4842  oprprc1 4908  fnoprabg 4941  oprabval2gf 4955  oprabval6g 4962  oprvconst2 4970  ndmoprg 4976  caoprmo 5003  1stval 5022  2ndval 5023  curry1 5075  curry2 5078  iotaval 5096  iotanul 5098  tz7.44-3 5138  rdgsucopab 5154  rdgsucopabn 5155  rdglim2 5157  fr0g 5160  frsucopab 5162  oa1suc 5209  om1 5223  oe1 5225  oarec 5244  oaabs 5309  map0b 5402  fodomr 5547  riotaiota 5566  riotaprc 5567  riotaund 5572  riotaclb 5573  mapenlem1 5583  mapenlem2 5584  xpmapenlem5 5594  phplem2 5603  unifi 5648  fodomfi 5656  suppr 5680  supsn 5681  supsnALT 5682  ordtypelem7 5690  tz9.12lem3 5772  rankonid 5806  rankxplim2 5824  oncardval 5865  omsubsuc 5877  ac6lem 5916  kmlem11 5937  zorn2 5958  cardval 5975  unxpdomlem 5995  nnacda 6088  1qec 6220  recrecpq 6225  ltaddpq 6231  ltexpq 6232  halfpq 6234  addclprlem1 6270  addclprlem2 6271  mulclprlem 6273  1idpr 6285  prlem934a 6289  prlem934b 6290  ltexprlem7 6300  ltaprlem 6302  prlem936a 6305  mulcmpblnrlem 6334  0idsr 6358  1idsr 6359  recexsrlem 6364  sqgt0sr 6367  ssgt0sr 6369  mulresr 6409  ax0id 6434  ax1id 6435  axcnre 6439  csbneggOLD 6521  negid 6536  ssxr 6714  divcan4zi 6937  lbinfm 7257  dfinfmr 7276  infmsup 7277  supxr 7290  supxrmnf 7296  uzindOLD 7420  quoremz 7492  quoremnn0 7494  intfracq 7496  ioojoin 7585  uzrdginii 7715  uzrdginip1i 7717  seq1suclem 7729  limsupval 7772  seq0valt 7779  seqzfval 7780  seq1seq01 7787  seq0p1 7794  seqzres2 7804  exp1 7816  expp1 7817  sqval 7854  discrlem2 7907  discrlem3 7908  sqrsqi 7970  crulem 7986  imre 8023  abs00i 8093  absidi 8112  cjdivi 8140  abs1mi 8156  faclbnd 8197  faclbnd2 8198  hashgval 8230  sumeqfv 8257  dffsum 8258  fsumserzfi 8260  serzfsum 8264  fsum1fi 8267  fsumadd 8282  csbfsum 8287  fsumshft 8291  binomlem1 8326  binomlem2 8327  binomlem4 8329  iserzexi 8406  dfisum 8452  isumvaltfi 8454  isumval2 8455  isum1clim 8458  isumcmpii 8476  geoisum 8504  geoisum1 8506  fsum0diag2 8521  divccncf 8542  eftlex 8640  ef1tlubi 8644  ef01tlubi 8648  absef01tlubi 8650  ef4p 8665  resinval 8698  recosval 8699  absefib 8750  efieq1re 8751  acdc3lem 8754  acdclem 8763  ruclem18 8796  ruclem19 8797  ruclem20 8798  ruclem21 8799  txtop 8934  txuni 8935  cnconst 9057  metssba 9086  metreslem 9099  metres 9100  blin 9129  opnfval 9134  methaus 9160  cncfmet 9183  remetdval 9186  bcthlem15 9291  bcth 9310  grpinvfval 9350  grpdivfval 9366  gxoprval 9380  resgrprn 9403  issubgi 9431  ghgrpilem1 9441  isga2 9452  gaid 9454  ssga 9455  gapm 9462  vcnegneg 9525  vafval 9554  bafval 9555  smfval 9556  0vfval 9557  vsfval 9586  nvnncan 9615  nvm1 9624  nvpi 9626  nvmtri 9631  imsval 9648  vacnlem5 9671  vacnlem6 9672  vacn 9673  nmcn 9678  ipfval 9691  ipval2 9696  ipcj 9706  ip1cnilem5 9716  sspval 9721  lnoval 9752  nmofval 9764  bloval 9781  0ofval 9787  nmlno0 9795  nmlnoubi 9796  ajfval 9809  hmoval 9810  ipdir 9843  ipass 9846  pythi 9851  ajfun 9862  minveclem19 9908  psref 9992  psrn 9993  spwval 10002  spwnex 10004  pilem3 10022  sinperlem1 10035  sin2pim 10041  cos2pim 10042  sinmpi 10043  cosmpi 10044  sinppi 10045  cosppi 10046  sinhalfpip 10048  sinhalfpim 10049  coshalfpip 10050  coshalfpim 10051  sineq0re 10067  shftefif1olem 10095  eflog 10114  logef 10116  symgoprv 10203  tx1cn 10223  tx2cn 10224  uptx 10226  2txcn 10229  subcld 10254  subtopmetlem 10255  fgf 10283  extbas2 10292  dirref 10355  dirge 10357  idrval 10374  on1el3 10412  hv2times 10560  bcseqi 10619  normpythi 10642  hhssnvt 10768  hhsssh 10772  pjthlem7 10858  pjoc1i 10897  chsupid 10944  h1de2i 11109  spanunsni 11135  cmcmlem 11167  cmbr3i 11176  fh1 11194  fh2 11195  hoival 11318  hoico1 11319  hoico2 11320  ho2times 11382  eigposi 11399  nmcopexlem2 11589  lnfnmuli 11610  nmcfnexlem2 11618  cnlnadjlem4 11640  cnlnadjlem5 11641  kbass5 11691  opsqrlem6 11716  pjnmopi 11719  pjclem3 11770  pjadj2coi 11777  sto1i 11808  strlem3a 11824  strlem4 11826  hstrlem3a 11832  hstrlem4 11834  dmdbr5 11880  mdexchi 11907  superpos 11926  atomli 11954  atcvatlem 11957  irredlem2 11963  irredlem3 11964  atabsi 11973  mdsymlem1 11975  dmdbr6ati 11995  bnj941 12842  bnj1144 12941  bnj961 13345  bnj1416 13528  bnj1463 13550  cayleylem2 13642  cayleythlem 13645  divalglem1 13697  divalglem9 13704  algr0 13740  algrp1lem 13741  eucalg 13755  ressn0 13829  fresin 13840  predep 13903  frsucopabn 13911  wfrlem4 13960  wfrlem13 13969  axdense 14027  axfelem15 14045  altopth2sn 14091  dmoprabss6 14336  dfoprab4spop 14339  imfstnrelc 14396  cmprelid2 14447  valfunun 14460  fvopab2b 14476  repcpwti 14503  iscst1 14519  preoref12 14569  dupos1 14586  gepsup 14593  seinf 14594  prodeqfv 14669  dffprod 14670  fprodserzfi 14672  fprod1fi 14675  clfsebsr 14709  fnopabco2b 14734  fprodsub 14742  trran2 14757  prsubrtr 14763  rngunval2 14774  sallnei 14873  homcard 14893  conttnf2 14945  tpgprop2 14987  trran 15014  domval 15070  codval 15071  idval 15072  cmpval 15073  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualded 15132  ishomd 15139  idsubfun 15206  valdom 15261  isplibg4a 15315  isplibg4b 15317  ordtypelem7OLD 15381  omsubsucOLD 15386  cldbnd 15410  clsun 15413  subsubtop 15423  compsub 15431  uncomp 15433  connsub 15443  isnrm2 15552  fixufil 15576  cnpfillim 15589  sfcls 15604  fcluscomplem 15620  tailf 15633  filnetlem5 15644  fvopabf4g 15703  resoprab2 15710  cocnv 15716  findcard2 15745  subspabs 15840  blssp 15844  mettrifi2 15848  piececn 15894  txcnoprab 15911  txopn 15913  cnopropabco 15917  cnoprab1 15921  cnoprab2 15922  ismtyres 15954  heiborlem9 15963  heiborlem11 15965  heiborlem18 15972  heiborlem35 15989  icccmp 16027  exidcl 16029  exidreslem 16030  phtpyco 16056  reparpht 16065  pcohtpy 16083  pcopt 16084  pcorev 16087  pltval 16781  pgeval 16794  lubfval 16803  glbfval 16808  joinfval 16814  meetfval 16821  p0val 16843  p1val 16844  cmtfval 16937  cvrfval 16987  patoms 17000  glbconx 17029  grpidvalNEW 17117  grpinvfvalNEW 17125  ringidval 17149  invrfval 17170  plusssfval 17204  ocvfval 17206  csubspset 17208  lineset 17219  pointset 17222  psubspset 17225  pmapfval 17236  pmapglb 17252  paddfval 17258  pmod2i 17310  polfval 17317  psubclset 17346  osumcllem3 17366  watomfval 17392  pautset 17395  dilfset 17401  trnfset 17404

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain