Theorem syl5eq 1518

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

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  syl5req 1519  syl5eqr 1520  3eqtr4g 1530  csbconstgf 2008  csbvarg 2019  csbiegft 2027  csbabg 2041  ssin 2230  uneqin 2254  prprc2 2451  difsnid 2465  opprc1 2496  sucprc 3041  orduniss2 3087  relop 3272  resabs1 3385  resabs2 3386  resopab2 3395  imasng 3421  ndmima 3431  xpdisj1 3465  xpdisj2 3466  resdisj 3468  rnxp 3469  unixp 3514  fnun 3591  fnresdisj 3594  f1orescnv 3701  fvprc 3718  fnrnfv 3756  fvopab4gf 3778  fvopabn 3783  fvopabgf 3784  fvopabnf 3785  fvsnun2 3793  elrnopabg 3797  fopab2 3820  rnssopab 3822  fopabco 3829  funiunfv 3863  tz7.44-3 3927  rdgsucopab 3943  rdgsucopabn 3944  rdglim2 3946  fr0t 3949  frsucopab 3951  oprprc1 3981  fnoprabg 4009  oprabval2gf 4023  oprabval6g 4029  oprvalconst2 4037  ndmoprg 4040  caoprmo 4067  1stval 4078  2ndval 4079  1st2val 4092  2nd2val 4093  curry1 4095  oa1suc 4161  om1 4173  oe1 4175  oarec 4193  oaabs 4249  map0b 4340  fodomr 4476  mapenlem1 4482  mapenlem2 4483  xpmapenlem5 4493  phplem2 4502  unifi 4545  fodomfi 4553  suppr 4577  supsn 4578  supsnALT 4579  tz9.12lem3 4648  rankonid 4682  rankxplim2 4700  ac6lem 4741  kmlem11 4762  zorn2 4783  oncardval 4806  cardval 4813  unxpdomlem 4830  1qec 5055  recrecpq 5060  ltaddpq 5066  ltexpq 5067  halfpq 5069  addclprlem1 5105  addclprlem2 5106  mulclprlem 5108  1idpr 5120  prlem934a 5124  prlem934b 5125  ltexprlem7 5135  ltaprlem 5137  prlem936a 5140  mulcmpblnrlem 5169  0idsr 5193  1idsr 5194  recexsrlem 5199  sqgt0sr 5202  ssgt0sr 5204  mulresr 5244  ax0id 5268  ax1id 5269  axcnre 5273  csbnegg 5351  negidt 5366  divcan4z 5731  lbinfm 6009  dfinfmr 6028  infmsup 6029  supxr 6042  supxrmnf 6048  uzindOLD 6170  uzrdgini 6258  uzrdginip1 6260  seq1suclem 6271  limsupvalt 6479  seq0valt 6486  seqzfval 6487  seq1seq0t 6494  seq0p1 6501  seqzres2 6511  exp1t 6523  expp1t 6524  sqvalt 6559  discrlem2 6607  discrlem3 6608  sqrsq 6671  crulem 6687  imret 6731  imretOLD 6732  abs00 6803  abs00OLD 6804  absid 6823  cjdiv 6853  abs1m 6869  faclbnd 6911  faclbnd2 6912  sumeqfv 6965  dffsum 6966  fsumserzf 6968  serzfsum 6972  fsum1f 6975  fsumadd 6990  csbfsum 6995  fsumshft 6999  binomlem1 7034  binomlem2 7035  binomlem4 7037  iserzex 7115  dfisum 7162  isumvaltf 7164  isumval2t 7165  isum1clim 7168  isumcmpi 7186  geoisum 7213  geoisum1 7215  fsum0diag2 7230  divccncf 7251  eftlext 7356  ef1tlub 7360  ef01tlub 7363  absef01tlub 7365  ef4pt 7377  resinvalt 7411  recosvalt 7412  acdc3lem 7464  acdclem 7472  ruclem18 7506  ruclem19 7507  ruclem20 7508  ruclem21 7509  cnconst 7759  metssba 7788  metreslem 7803  metres 7804  blin 7834  opnfval 7840  methaus 7865  cncfmet 7888  remetdval 7891  bcthlem15 7996  bcth 8015  grpidval 8041  grpinvfval 8049  grpdivfval 8064  resgrprn 8078  issubgi 8107  ghgrpilem1 8118  vcnegneg 8178  vafval 8207  bafval 8208  smfval 8209  0vfval 8210  vsfval 8239  nvnncan 8268  nvm1 8277  nvpi 8279  nvmtri 8284  imsval 8302  nmcn 8325  ipfval 8338  ipval2 8343  ipcj 8353  ip1cnilem5 8363  sspval 8368  lnoval 8399  nmofval 8410  bloval 8426  0ofval 8432  nmlno0 8440  nmlnoubi 8441  ajfval 8453  hmoval 8454  ipdir 8486  ipass 8489  pythi 8494  ajfun 8505  minveclem19 8547  psref 8632  psrn 8633  spwval 8642  spwnex 8644  pilem3 8656  sinperlem1 8669  sin2pim 8675  cos2pim 8676  sinmpi 8677  cosmpi 8678  sinhalfpip 8680  sinhalfpim 8681  coshalfpip 8682  coshalfpim 8683  circoprvalOLD 8721  shftefif1olem 8725  eflogt 8744  logeft 8746  hv2timest 8912  bcseq 8970  normpyth 8993  hhssnvt 9123  hhsssh 9127  pjthlem7 9213  pjoc1 9252  chsupid 9299  h1de2 9464  spanunsn 9492  cmcmlem 9524  cmbr3 9533  fh1t 9551  fh2t 9552  hoivalt 9672  hoico1t 9673  hoico2t 9674  ho2timest 9736  eigpos 9753  nmcopexlem2 9943  lnfnmul 9964  nmcfnexlem2 9972  cnlnadjlem4 9994  cnlnadjlem5 9995  kbass5t 10044  pjnmop 10066  pjclem3 10116  pjadj2co 10123  sto1 10154  strlem3a 10170  strlem4 10172  hstrlem3a 10178  hstrlem4 10180  dmdbr5 10226  mdexch 10253  superpos 10272  atoml 10300  atcvatlem 10303  irredlem2 10309  irredlem3 10310  atabs 10319  mdsymlem1 10321  dmdbr6at 10341  symgoprval 10395  cayleylem2 10401  cayleythlem 10404  fvopab2a 10452  homcard 10520  limfillem2 10559  trran 10587  domval 10606  codval 10607  idval 10608  cmpval 10609  ishomd 10669

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

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

Copyright terms: Public domain