Theorem cleqan12rd 1117

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

Hypotheses

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

Assertion

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

Proof of Theorem cleqan12rd

Step	Hyp	Ref	Expression
1		cleqan12rd.1	. . 3 |- (ph -> A = B)
2		cleqan12rd.2	. . 3 |- (ps -> C = D)
3	1, 2	cleqan12d 1116	. 2 |- ((ph /\ ps) -> (A = C <-> B = D))
4	3	ancoms 334	1 |- ((ps /\ ph) -> (A = C <-> B = D))

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

This theorem is referenced by:  fvopabgf 2874  fvopabnf 2875  tfrlem5 2953  inf3lema 3460  numth 3599  zorn 3611

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