Theorem eqeqan12rd 2157

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 2156	. 2 |- ((ph /\ ps) -> (A = C <-> B = D))
4	3	ancoms 416	1 |- ((ps /\ ph) -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   = wceq 1586

This theorem is referenced by:  fvopab4gf 4830  fvopabgf 4836  fvopabnf 4837  tfrlem5 5287  inf3lema 5947  aceq8a 6199  numth 6356  zorn2 6369  mulgcdlem2 9352  fsumcnlem 10133  effoi 10970  eigorthi 12232  prtoptop 15684  bfplem3 16824

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-17 1605  ax-4 1608  ax-5o 1610  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-an 339  df-cleq 2134

Copyright terms: Public domain