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 956

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 3042  orduniss2 3088  relop 3273  resabs1 3386  resabs2 3387  resopab2 3396  imasng 3422  ndmima 3432  xpdisj1 3466  xpdisj2 3467  resdisj 3469  rnxp 3470  unixp 3515  fnun 3592  fnresdisj 3595  f1orescnv 3702  fvprc 3719  fnrnfv 3757  fvopab4gf 3779  fvopabn 3784  fvopabgf 3785  fvopabnf 3786  fvsnun2 3794  elrnopabg 3798  fopab2 3821  rnssopab 3823  fopabco 3830  funiunfv 3864  tz7.44-3 3928  rdgsucopab 3944  rdgsucopabn 3945  rdglim2 3947  fr0t 3950  frsucopab 3952  oprprc1 3982  fnoprabg 4010  oprabval2gf 4024  oprabval6g 4030  oprvalconst2 4038  ndmoprg 4041  caoprmo 4068  1stval 4079  2ndval 4080  1st2val 4093  2nd2val 4094  curry1 4096  oa1suc 4162  om1 4174  oe1 4176  oarec 4194  oaabs 4250  map0b 4341  fodomr 4477  mapenlem1 4483  mapenlem2 4484  xpmapenlem5 4494  phplem2 4503  unifi 4546  fodomfi 4554  suppr 4578  supsn 4579  supsnALT 4580  tz9.12lem3 4649  rankonid 4683  rankxplim2 4701  ac6lem 4742  kmlem11 4763  zorn2 4784  oncardval 4807  cardval 4814  unxpdomlem 4831  1qec 5056  recrecpq 5061  ltaddpq 5067  ltexpq 5068  halfpq 5070  addclprlem1 5106  addclprlem2 5107  mulclprlem 5109  1idpr 5121  prlem934a 5125  prlem934b 5126  ltexprlem7 5136  ltaprlem 5138  prlem936a 5141  mulcmpblnrlem 5170  0idsr 5194  1idsr 5195  recexsrlem 5200  sqgt0sr 5203  ssgt0sr 5205  mulresr 5245  ax0id 5269  ax1id 5270  axcnre 5274  csbnegg 5352  negidt 5367  divcan4z 5732  lbinfm 6016  dfinfmr 6035  infmsup 6036  supxr 6049  supxrmnf 6055  uzindOLD 6176  uzrdgini 6267  uzrdginip1 6269  seq1suclem 6280  ioojoint 6376  limsupvalt 6489  seq0valt 6496  seqzfval 6497  seq1seq0t 6504  seq0p1 6511  seqzres2 6521  exp1t 6533  expp1t 6534  sqvalt 6569  discrlem2 6617  discrlem3 6618  sqrsq 6680  crulem 6696  imret 6733  abs00 6800  absid 6819  cjdiv 6846  abs1m 6862  faclbnd 6903  faclbnd2 6904  sumeqfv 6955  dffsum 6956  fsumserzf 6958  serzfsum 6962  fsum1f 6965  fsumadd 6980  csbfsum 6985  fsumshft 6989  binomlem1 7024  binomlem2 7025  binomlem4 7027  iserzex 7104  dfisum 7149  isumvaltf 7151  isumval2t 7152  isum1clim 7155  isumcmpi 7173  geoisum 7200  geoisum1 7202  fsum0diag2 7217  divccncf 7238  eftlext 7336  ef1tlub 7340  ef01tlub 7344  absef01tlub 7346  ef4pt 7358  resinvalt 7390  recosvalt 7391  acdc3lem 7443  acdclem 7451  ruclem18 7484  ruclem19 7485  ruclem20 7486  ruclem21 7487  cnconst 7737  metssba 7766  metreslem 7779  metres 7780  blin 7809  opnfval 7814  methaus 7839  cncfmet 7862  remetdval 7865  bcthlem15 7970  bcth 7989  grpidval 8015  grpinvfval 8023  grpdivfval 8038  resgrprn 8052  issubgi 8079  ghgrpilem1 8090  vcnegneg 8150  vafval 8179  bafval 8180  smfval 8181  0vfval 8182  vsfval 8211  nvnncan 8240  nvm1 8249  nvpi 8251  nvmtri 8256  imsval 8273  nmcn 8296  ipfval 8309  ipval2 8314  ipcj 8324  ip1cnilem5 8334  sspval 8339  lnoval 8370  nmofval 8382  bloval 8398  0ofval 8404  nmlno0 8412  nmlnoubi 8413  ajfval 8426  hmoval 8427  ipdir 8459  ipass 8462  pythi 8467  ajfun 8478  minveclem19 8520  psref 8606  psrn 8607  spwval 8616  spwnex 8618  pilem3 8630  sinperlem1 8643  sin2pim 8649  cos2pim 8650  sinmpi 8651  cosmpi 8652  sinhalfpip 8656  sinhalfpim 8657  coshalfpip 8658  coshalfpim 8659  shftefif1olem 8696  eflogt 8715  logeft 8717  hv2timest 8883  bcseq 8941  normpyth 8964  hhssnvt 9090  hhsssh 9094  pjthlem7 9180  pjoc1 9219  chsupid 9266  h1de2 9431  spanunsn 9457  cmcmlem 9489  cmbr3 9498  fh1t 9516  fh2t 9517  hoivalt 9636  hoico1t 9637  hoico2t 9638  ho2timest 9700  eigpos 9717  nmcopexlem2 9907  lnfnmul 9928  nmcfnexlem2 9936  cnlnadjlem4 9958  cnlnadjlem5 9959  kbass5t 10008  pjnmop 10030  pjclem3 10080  pjadj2co 10087  sto1 10118  strlem3a 10134  strlem4 10136  hstrlem3a 10142  hstrlem4 10144  dmdbr5 10190  mdexch 10217  superpos 10236  atoml 10264  atcvatlem 10267  irredlem2 10273  irredlem3 10274  atabs 10283  mdsymlem1 10285  dmdbr6at 10305  symgoprval 10359  cayleylem2 10365  cayleythlem 10368  fvopab2a 10413  homcard 10481  limfillem2 10520  trran 10548  domval 10567  codval 10568  idval 10569  cmpval 10570  ishomd 10630

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain