This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∩ C = B ∩ D

Proof

Step Hyp Ref Expression
1 ineq1i.1 ⊢ A = B
2 ineq12i.2 ⊢ C = D
3 ineq12 ⊢ A = B ∧ C = D → A ∩ C = B ∩ D
4 1 2 3 mp2an ⊢ A ∩ C = B ∩ D