Theorem cleqan12rd 1117

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

Hypotheses

Ref	Expression
cleqan12rd.1	⊢ (φ → A = B)
cleqan12rd.2	⊢ (ψ → C = D)

Assertion

Ref	Expression
cleqan12rd	⊢ ((ψ ∧ φ) → (A = C ↔ B = D))

Proof of Theorem cleqan12rd

Step	Hyp	Ref	Expression
1		cleqan12rd.1	. . 3 ⊢ (φ → A = B)
2		cleqan12rd.2	. . 3 ⊢ (ψ → C = D)
3	1, 2	cleqan12d 1116	. 2 ⊢ ((φ ∧ ψ) → (A = C ↔ B = D))
4	3	ancoms 334	1 ⊢ ((ψ ∧ φ) → (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