Metamath Proof Explorer


Theorem resabs2d

Description: Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis resabs2d.1 φBC
Assertion resabs2d φABC=AB

Proof

Step Hyp Ref Expression
1 resabs2d.1 φBC
2 resabs2 BCABC=AB
3 1 2 syl φABC=AB