Metamath Proof Explorer


Theorem ineqan12d

Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007)

Ref Expression
Hypotheses ineq1d.1 φ A = B
ineqan12d.2 ψ C = D
Assertion ineqan12d φ ψ A C = B D

Proof

Step Hyp Ref Expression
1 ineq1d.1 φ A = B
2 ineqan12d.2 ψ C = D
3 ineq12 A = B C = D A C = B D
4 1 2 3 syl2an φ ψ A C = B D