Theorem eqeqan12rd 1903

Description: A useful inference for substituting definitions into an equality.

Hypotheses

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

Assertion

Ref	Expression
eqeqan12rd	|- ((ps /\ ph) -> (A = C <-> B = D))

Proof of Theorem eqeqan12rd

Step	Hyp	Ref	Expression
1		eqeqan12rd.1	. . 3 |- (ph -> A = B)
2		eqeqan12rd.2	. . 3 |- (ps -> C = D)
3	1, 2	eqeqan12d 1901	. 2 |- ((ph /\ ps) -> (A = C <-> B = D))
4	3	ancoms 484	1 |- ((ps /\ ph) -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298

This theorem is referenced by:  fvopab4gf 4744  fvopabgf 4750  fvopabnf 4751  tfrlem5 5123  inf3lema 5715  numth 5946  zorn2 5958  fsumcnlem 9267  effoi 10099  eigorthi 11400  mulgcdlem2 13757  prtoptop 14919  bfplem3 16000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain