Metamath Proof Explorer


Theorem resabs2

Description: Absorption law for restriction. (Contributed by NM, 27-Mar-1998)

Ref Expression
Assertion resabs2 B C A B C = A B

Proof

Step Hyp Ref Expression
1 rescom A B C = A C B
2 resabs1 B C A C B = A B
3 1 2 eqtrid B C A B C = A B