Metamath Proof Explorer


Theorem ineq12i

Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004) (Proof shortened by Eric Schmidt, 26-Jan-2007)

Ref Expression
Hypotheses ineq1i.1 A=B
ineq12i.2 C=D
Assertion ineq12i AC=BD

Proof

Step Hyp Ref Expression
1 ineq1i.1 A=B
2 ineq12i.2 C=D
3 ineq12 A=BC=DAC=BD
4 1 2 3 mp2an AC=BD