Theorem sylan9eqr 1145

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
sylan9eqr	|- ((ps /\ ph) -> A = C)

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 |- (ph -> A = B)
2		sylan9eqr.2	. . 3 |- (ps -> B = C)
3	1, 2	sylan9eq 1144	. 2 |- ((ph /\ ps) -> A = C)
4	3	ancoms 334	1 |- ((ps /\ ph) -> A = C)

Syntax hints:   -> wi 2   /\ wa 196   = wceq 1091

This theorem is referenced by:  opprc3 1908  onuninsuc 2356  limsuclem 2360  abianfplem 2999  caoprmo 3084  oesuc 3134  oawordeulem 3156  nnmass 3181  sbthlem4 3352  sbthlem6 3354  mapenlem1 3384  mapdom2 3389  mapunen 3397  ssenen 3399  r1val1 3502  rankonid 3538  unxpdomlem 3649  cardaleph 3690  ltexpq 3874  addclprlem1 3912  mulclprlem 3915  1idpr 3927  prlem934a 3931  prlem936a 3947  prlem936 3949  reclem3pr 3952  mulcmpblnrlem 3976  recexsrlem 4006  ssgt0sr 4011  ax1id 4077  negeu 4124  pncant 4161  receu 4215  nn0addclt 4551  qaddclt 4642  qmulclt 4644  qrecclt 4646  discrlem3 4715  hiidge0t 5056  normgt0t 5078  hsn0elch 5155  shscl 5282  spansneleq 5475  h1datom 5483  spansncv 5542  5oalem1 5544  3oalem2 5553  sumdmdlem 5786

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