Theorem syl5eq 1136

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 7	. 2 |- (ph -> C = A)
3		syl5eq.1	. 2 |- (ph -> A = B)
4	2, 3	eqtrd 1128	1 |- (ph -> C = B)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  syl5req 1137  syl5eqr 1138  3eqtr4g 1147  ssin 1659  prex 1892  opprc1 1905  supsn 2168  sucprc 2297  imasn 2616  ndmima 2623  xpdisj1 2653  xpdisj2 2654  resdisj 2656  rnxp 2657  fnun 2730  fnresdisj 2732  fconst 2774  fvprc 2829  fniunfv 2860  fvopabn 2873  fvopabgf 2874  fvopabnf 2875  elrnopab 2884  fopab2 2891  tz7.44-3 2968  rdgsucopab 2984  rdgsucopabn 2985  rdglim2 2987  frzer 2990  frsucopab 2992  oprprc1 3019  ndmoprg 3057  caoprmo 3084  1stval 3089  2ndval 3090  1st2val 3097  oa1suc 3132  om1 3144  oe1 3146  map0b 3267  mapenlem1 3384  mapenlem2 3385  xpmapenlem5 3395  phplem3 3405  tz9.12lem3 3505  rankonid 3538  ac6lem 3575  kmlem10 3589  zorn 3611  fodomb 3615  oncardval 3626  cardval 3633  unxpdomlem 3649  1qec 3862  recrecpq 3867  ltaddpq 3873  ltexpq 3874  halfpq 3876  addclprlem1 3912  addclprlem2 3913  mulclprlem 3915  1idpr 3927  prlem934a 3931  prlem934b 3932  ltexprlem7 3942  ltaprlem 3944  prlem936a 3947  mulcmpblnrlem 3976  0idsr 4000  1idsr 4001  recexsrlem 4006  sqgt0sr 4009  ssgt0sr 4011  mulresr 4051  ax0id 4076  ax1id 4077  axrecex 4079  axcnre 4087  divcan4z 4250  crulem 4528  uzind 4603  uzrdgini 4658  seqsuclem 4669  exp1t 4679  exp2t 4683  discrlem2 4714  discrlem3 4715  sqrsqe 4774  abs00 4839  absid 4850  ruclem8 4892  ruclem18 4902  ruclem19 4903  ruclem20 4904  ruclem21 4905  bcseq 5073  normpyth 5090  pjthlem7 5231  pjoc1 5268  chsupid 5312  h1de2 5458  spanunsn 5482  cmcmlem 5500  cmbr3 5509  pjclem3 5651  pjadj2co 5656  sto1 5677  strlem3a 5693  strlem4 5695  atcvatlem 5770  mdsymlem1 5776

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org