HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syl5eq 1511
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
StepHypRef Expression
1 syl5eq.2 . . 3 |- C = A
21a1i 8 . 2 |- (ph -> C = A)
3 syl5eq.1 . 2 |- (ph -> A = B)
42, 3eqtrd 1499 1 |- (ph -> C = B)
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 953
This theorem is referenced by:  syl5req 1512  syl5eqr 1513  3eqtr4g 1523  csbconstgf 2000  csbvarg 2011  csbiegft 2019  csbabg 2033  ssin 2222  uneqin 2246  prprc2 2444  difsnid 2458  opprc1 2489  sucprc 3034  orduniss2 3080  relop 3265  resabs1 3372  resabs2 3373  resopab2 3382  imasng 3408  ndmima 3418  xpdisj1 3454  xpdisj2 3455  resdisj 3457  rnxp 3458  unixp 3503  fnun 3580  fnresdisj 3583  f1orescnv 3689  fvprc 3706  fnrnfv 3744  fvopab4gf 3766  fvopabn 3771  fvopabgf 3772  fvopabnf 3773  fvsnun2 3781  elrnopabg 3785  fopab2 3808  rnssopab 3810  fopabco 3817  funiunfv 3851  tz7.44-3 3915  rdgsucopab 3931  rdgsucopabn 3932  rdglim2 3934  fr0t 3937  frsucopab 3939  oprprc1 3969  fnoprabg 3997  oprabval2gf 4011  oprabval6g 4017  oprvalconst2 4025  ndmoprg 4028  ndmoprgOLD 4029  caoprmo 4056  1stval 4065  2ndval 4066  1st2val 4079  2nd2val 4080  curry1 4082  oa1suc 4148  om1 4160  oe1 4162  oarec 4180  oaabs 4236  map0b 4327  fodomr 4463  mapenlem1 4469  mapenlem2 4470  xpmapenlem5 4480  phplem2 4489  unifi 4532  fodomfi 4540  suppr 4562  supsn 4563  supsnALT 4564  tz9.12lem3 4633  rankonid 4667  rankxplim2 4685  ac6lem 4726  kmlem11 4747  zorn2 4768  oncardval 4791  cardval 4798  unxpdomlem 4815  1qec 5040  recrecpq 5045  ltaddpq 5051  ltexpq 5052  halfpq 5054  addclprlem1 5090  addclprlem2 5091  mulclprlem 5093  1idpr 5105  prlem934a 5109  prlem934b 5110  ltexprlem7 5120  ltaprlem 5122  prlem936a 5125  mulcmpblnrlem 5154  0idsr 5178  1idsr 5179  recexsrlem 5184  sqgt0sr 5187  ssgt0sr 5189  mulresr 5229  ax0id 5253  ax1id 5254  axcnre 5258  csbnegg 5336  negidt 5351  divcan4z 5717  lbinfm 5995  dfinfmr 6014  infmsup 6015  supxr 6028  supxrmnf 6034  uzindOLD 6156  uzrdgini 6240  uzrdginip1 6242  seq1suclem 6253  limsupvalt 6461  seq0valt 6468  seqzfval 6469  seq1seq0t 6476  seq0p1 6483  seqzres2 6493  exp1t 6505  expp1t 6506  sqvalt 6540  discrlem2 6587  discrlem3 6588  sqrsq 6650  crulem 6666  imret 6710  abs00 6777  absid 6796  cjdiv 6826  abs1m 6841  faclbnd 6882  faclbnd2 6883  sumeqfv 6935  dffsum 6936  fsumserzf 6938  serzfsum 6942  fsum1f 6945  fsumadd 6960  csbfsum 6965  fsumshft 6969  binomlem1 7004  binomlem2 7005  binomlem4 7007  iserzex 7082  dfisum 7127  isumvaltf 7129  isumval2t 7130  isumcmpi 7150  geoisum 7177  geoisum1 7179  fsum0diag2 7194  divccncf 7215  eftlext 7320  ef1tlub 7324  ef01tlub 7327  absef01tlub 7329  ef4pt 7341  resinvalt 7375  recosvalt 7376  acdc3lem 7428  acdclem 7436  ruclem18 7470  ruclem19 7471  ruclem20 7472  ruclem21 7473  cnconst 7719  metssba 7748  metreslem 7762  metres 7763  blin 7792  opnfval 7797  methaus 7821  cncfmet 7844  remetdval 7847  bcthlem15 7947  bcth 7966  grpidval 7992  grpinvfval 8000  grpdivfval 8016  resgrprn 8030  issubgi 8059  ghgrpilem1 8070  vcnegneg 8130  vafval 8160  bafval 8161  smfval 8162  0vfval 8163  vsfval 8194  nvnncan 8223  nvm1 8231  nvpi 8233  nvmtri 8238  imsval 8254  nmcn 8274  ipfval 8286  ipval2 8291  ipcj 8301  ip1cnilem5 8311  sspval 8316  lnoval 8347  nmofval 8357  bloval 8373  0ofval 8379  nmlno0 8387  nmlnoubi 8388  ajfval 8400  hmoval 8401  ipdir 8433  ipass 8436  pythi 8441  ajfun 8452  minveclem19 8494  psref 8575  spwval 8582  pilem3 8592  sinperlem1 8605  sin2pim 8611  cos2pim 8612  sinmpi 8613  cosmpi 8614  sinhalfpip 8616  sinhalfpim 8617  coshalfpip 8618  coshalfpim 8619  circoprvalOLD 8657  shftefif1olem 8661  shftefif1olemOLD 8662  eflogt 8682  logeft 8684  hv2timest 8849  bcseq 8907  normpyth 8930  hhssnvt 9055  hhsssh 9059  pjthlem7 9140  pjoc1 9179  chsupid 9226  h1de2 9391  spanunsn 9419  cmcmlem 9451  cmbr3 9460  fh1t 9478  fh2t 9479  hoivalt 9598  hoico1t 9599  hoico2t 9600  ho2timest 9662  eigpos 9679  nmcopexlem2 9867  lnfnmul 9888  nmcfnexlem2 9896  cnlnadjlem4 9918  cnlnadjlem5 9919  kbass5t 9965  pjnmop 9986  pjclem3 10035  pjadj2co 10042  sto1 10073  strlem3a 10089  strlem4 10091  hstrlem3a 10097  hstrlem4 10099  mdexch 10170  superpos 10189  atoml 10217  atcvatlem 10220  irredlem2 10226  irredlem3 10227  atabs 10236  mdsymlem1 10238  dmdbr6at 10256  symgoprval 10309  cayleylem2 10317  cayleythlem 10320  fvopab2a 10359  homcard 10426  trran 10480  domval 10499  codval 10500  idval 10501  cmpval 10502  ishomd 10562
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462
Copyright terms: Public domain