Theorem syl5eqr 2218

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl5eqr	|- (ph -> A = C)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 |- B = A
2	1	eqcomi 2174	. 2 |- A = B
3		syl5eqr.2	. 2 |- (ph -> B = C)
4	2, 3	syl5eq 2214	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 1615

This theorem is referenced by:  syl5eqrOLD 2219  3eqtr3g 2229  csbeq1a 2811  pofun 3795  reuunixfr 4028  coires1 4551  fnexALT 4671  f1imacnv 4778  foimacnv 4779  funfv 4855  dffv2 4859  fsn2 4942  funiunfv 4976  funiunfvf 4977  sbcopeq1a 5202  csbopeq1a 5203  dfoprab5s 5208  df1st2 5231  df2nd2 5232  fparlem3 5246  fparlem4 5247  oasuc 5414  omsuc 5416  oesuc 5417  omxpenlem 5712  pw2en 5714  sbthlem8 5726  sbthlem9 5727  fodomr 5759  riotaxfrd 5801  xpfi 5911  fiint 5916  ordtypelem7 5965  inf3lem7OLD 6002  infxpenlem 6212  omsubsuc 6233  nnaun2 6330  axdc4lem 6381  fodom 6448  prlem934a 6732  reclem3pr 6753  pn0sr 6805  mulgt0sr 6809  supsrlem2 6821  addid2 7083  addgegt0i 7231  add20i 7233  mulge0i 7237  recdiv 7400  prodgt0i 7430  fseq1p1m1lem2 8177  fseq1p1m1lem3 8178  fzshftral 8186  shftidt 8259  sqrcli 8450  sqrge0i 8452  rimul 8494  bcpasci 8722  fsumserz2 8775  fsump1i 8778  fsumshft 8803  iserzabslem 8950  isumval2 8967  isumclim4 8974  isumshfti 8977  isumshft2i 8978  geoisum1c 9023  ivthlem8 9066  eirrlem5 9171  cos01bndlem3 9253  acdc3lem 9270  acdclem 9279  eucalg 9486  cnconst 10073  remetdval 10202  ssga 10476  gapm 10483  nvpi 10647  nvop 10658  phop 10841  ubthlem6 10900  minvec34 10922  minvec34OLD 10923  filintf 11270  fbssint 11275  hausfillim 11299  hi01 11590  pjchi 11890  chjidm 12068  mayete3i 12298  mayete3OLDi 12299  ho0val 12303  lnop0 12517  opsqrlem5 12704  pjin2i 12755  mdslmd3i 12893  mdexchi 12896  bnj1387 14455  ltexnq 14578  hashpwlem 14610  axfelem18 14963  f2imacnv 15326  cmpdiaOLD 15426  islatalg 15531  fprodp1i 15674  fnopabco2b 15730  intopcoaconc 15924  rcfpfillem6 15960  ishomb 16192  isfuna 16237  isseg1 16375  ordtypelem7OLD 16466  omsubsucOLD 16471  opncldf1 16487  connsub 16528  comppfsc 16602  neibastop2lem4 16607  ufileu 16658  filufint 16659  fclsfnflim 16699  fcluscomplem 16705  filnetlem5 16729  cocnv 16801  pofunOLD 16857  cnimass 16973  cnss 16977  paste 16978  pcorev 17172  pi1bval 17173  pi1fval 17177  osumcllem9 18649  4atexlemex2 18828  cdleme20j 18986  cdlemg47 19410

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1622  ax-17 1634  ax-4 1637  ax-5o 1639  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-cleq 2163

Copyright terms: Public domain