Theorem sylan9req 1528

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylan9req

Step	Hyp	Ref	Expression
1		sylan9req.1	. . 3 |- (ph -> B = A)
2	1	eqcomd 1480	. 2 |- (ph -> A = B)
3		sylan9req.2	. 2 |- (ps -> B = C)
4	2, 3	sylan9eq 1527	1 |- ((ph /\ ps) -> A = C)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956

This theorem is referenced by:  fndmu 3589  fodmrnu 3680  fvopab4gf 3781  fvopabgf 3787  fvopabnf 3788  oprabval2gf 4026  mapunen 4502  nndivt 5959  fsum1 7005  fsum1f 7007  fsump1f 7011  infxpidmlem10 7561  retopbas 7655  metxp 7834  grpidinvlem4 8051  efifolem2 8723  dmdsl3t 10242  atoml2 10310

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