Metamath Proof Explorer


Theorem ineq1d

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994)

Ref Expression
Hypothesis ineq1d.1 φA=B
Assertion ineq1d φAC=BC

Proof

Step Hyp Ref Expression
1 ineq1d.1 φA=B
2 ineq1 A=BAC=BC
3 1 2 syl φAC=BC