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 i^i C ) = ( B i^i D )

Proof

Step Hyp Ref Expression
1 ineq1i.1 
 |-  A = B
2 ineq12i.2 
 |-  C = D
3 ineq12 
 |-  ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )
4 1 2 3 mp2an 
 |-  ( A i^i C ) = ( B i^i D )