Theorem syl5eq 1516

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 1504	1 |- (ph -> C = B)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  syl5req 1517  syl5eqr 1518  3eqtr4g 1528  csbconstgf 2006  csbvarg 2017  csbiegft 2025  csbabg 2039  ssin 2228  uneqin 2252  prprc2 2449  difsnid 2463  opprc1 2494  sucprc 3039  orduniss2 3085  relop 3270  resabs1 3380  resabs2 3381  resopab2 3390  imasng 3416  ndmima 3426  xpdisj1 3460  xpdisj2 3461  resdisj 3463  rnxp 3464  unixp 3509  fnun 3586  fnresdisj 3589  f1orescnv 3695  fvprc 3712  fnrnfv 3750  fvopab4gf 3772  fvopabn 3777  fvopabgf 3778  fvopabnf 3779  fvsnun2 3787  elrnopabg 3791  fopab2 3814  rnssopab 3816  fopabco 3823  funiunfv 3857  tz7.44-3 3921  rdgsucopab 3937  rdgsucopabn 3938  rdglim2 3940  fr0t 3943  frsucopab 3945  oprprc1 3975  fnoprabg 4003  oprabval2gf 4017  oprabval6g 4023  oprvalconst2 4031  ndmoprg 4034  ndmoprgOLD 4035  caoprmo 4062  1stval 4071  2ndval 4072  1st2val 4085  2nd2val 4086  curry1 4088  oa1suc 4154  om1 4166  oe1 4168  oarec 4186  oaabs 4242  map0b 4333  fodomr 4469  mapenlem1 4475  mapenlem2 4476  xpmapenlem5 4486  phplem2 4495  unifi 4538  fodomfi 4546  suppr 4570  supsn 4571  supsnALT 4572  tz9.12lem3 4641  rankonid 4675  rankxplim2 4693  ac6lem 4734  kmlem11 4755  zorn2 4776  oncardval 4799  cardval 4806  unxpdomlem 4823  1qec 5048  recrecpq 5053  ltaddpq 5059  ltexpq 5060  halfpq 5062  addclprlem1 5098  addclprlem2 5099  mulclprlem 5101  1idpr 5113  prlem934a 5117  prlem934b 5118  ltexprlem7 5128  ltaprlem 5130  prlem936a 5133  mulcmpblnrlem 5162  0idsr 5186  1idsr 5187  recexsrlem 5192  sqgt0sr 5195  ssgt0sr 5197  mulresr 5237  ax0id 5261  ax1id 5262  axcnre 5266  csbnegg 5344  negidt 5359  divcan4z 5725  lbinfm 6003  dfinfmr 6022  infmsup 6023  supxr 6036  supxrmnf 6042  uzindOLD 6164  uzrdgini 6248  uzrdginip1 6250  seq1suclem 6261  limsupvalt 6469  seq0valt 6476  seqzfval 6477  seq1seq0t 6484  seq0p1 6491  seqzres2 6501  exp1t 6513  expp1t 6514  sqvalt 6548  discrlem2 6595  discrlem3 6596  sqrsq 6658  crulem 6674  imret 6718  abs00 6785  absid 6804  cjdiv 6834  abs1m 6849  faclbnd 6890  faclbnd2 6891  sumeqfv 6943  dffsum 6944  fsumserzf 6946  serzfsum 6950  fsum1f 6953  fsumadd 6968  csbfsum 6973  fsumshft 6977  binomlem1 7012  binomlem2 7013  binomlem4 7015  iserzex 7090  dfisum 7135  isumvaltf 7137  isumval2t 7138  isumcmpi 7158  geoisum 7185  geoisum1 7187  fsum0diag2 7202  divccncf 7223  eftlext 7328  ef1tlub 7332  ef01tlub 7335  absef01tlub 7337  ef4pt 7349  resinvalt 7383  recosvalt 7384  acdc3lem 7436  acdclem 7444  ruclem18 7478  ruclem19 7479  ruclem20 7480  ruclem21 7481  cnconst 7730  metssba 7759  metreslem 7774  metres 7775  blin 7804  opnfval 7809  methaus 7834  cncfmet 7857  remetdval 7860  bcthlem15 7963  bcth 7982  grpidval 8008  grpinvfval 8016  grpdivfval 8031  resgrprn 8045  issubgi 8074  ghgrpilem1 8085  vcnegneg 8145  vafval 8174  bafval 8175  smfval 8176  0vfval 8177  vsfval 8206  nvnncan 8235  nvm1 8244  nvpi 8246  nvmtri 8251  imsval 8267  nmcn 8287  ipfval 8299  ipval2 8304  ipcj 8314  ip1cnilem5 8324  sspval 8329  lnoval 8360  nmofval 8370  bloval 8386  0ofval 8392  nmlno0 8400  nmlnoubi 8401  ajfval 8413  hmoval 8414  ipdir 8446  ipass 8449  pythi 8454  ajfun 8465  minveclem19 8507  psref 8592  spwval 8600  spwnex 8602  pilem3 8611  sinperlem1 8624  sin2pim 8630  cos2pim 8631  sinmpi 8632  cosmpi 8633  sinhalfpip 8635  sinhalfpim 8636  coshalfpip 8637  coshalfpim 8638  circoprvalOLD 8676  shftefif1olem 8680  eflogt 8699  logeft 8701  hv2timest 8867  bcseq 8925  normpyth 8948  hhssnvt 9074  hhsssh 9078  pjthlem7 9163  pjoc1 9202  chsupid 9249  h1de2 9414  spanunsn 9442  cmcmlem 9474  cmbr3 9483  fh1t 9501  fh2t 9502  hoivalt 9621  hoico1t 9622  hoico2t 9623  ho2timest 9685  eigpos 9702  nmcopexlem2 9890  lnfnmul 9911  nmcfnexlem2 9919  cnlnadjlem4 9941  cnlnadjlem5 9942  kbass5t 9991  pjnmop 10013  pjclem3 10063  pjadj2co 10070  sto1 10101  strlem3a 10117  strlem4 10119  hstrlem3a 10125  hstrlem4 10127  mdexch 10199  superpos 10218  atoml 10246  atcvatlem 10249  irredlem2 10255  irredlem3 10256  atabs 10265  mdsymlem1 10267  dmdbr6at 10285  symgoprval 10338  cayleylem2 10344  cayleythlem 10347  fvopab2a 10395  homcard 10462  trran 10516  domval 10535  codval 10536  idval 10537  cmpval 10538  ishomd 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain