Metamath Proof Explorer


Theorem mrcidmd

Description: Moore closure is idempotent. Deduction form of mrcidm . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrcssidd.1 φAMooreX
mrcssidd.2 N=mrClsA
mrcssidd.3 φUX
Assertion mrcidmd φNNU=NU

Proof

Step Hyp Ref Expression
1 mrcssidd.1 φAMooreX
2 mrcssidd.2 N=mrClsA
3 mrcssidd.3 φUX
4 2 mrcidm AMooreXUXNNU=NU
5 1 3 4 syl2anc φNNU=NU