diff --git a/set.mm b/set.mm
index d39cccbe83..9573ce4691 100644
--- a/set.mm
+++ b/set.mm
@@ -571200,6 +571200,18 @@ Real and complex numbers (cont.)
   currybi $p |- ( ( ph <-> ( ph <-> ps ) ) -> ps ) $=
     ( wb biid biass biimpri mpbii ) AABCCZAACZBADIBCHAABEFG $.
 
+  $( Suppose ` ph ` , ` ps ` are distinct atomic propositional formulas, and
+     let ` _G ` be the smallest class of formulas for which ` T. e. _G ` and
+     ` ( ch -> ph ) ` , ` ( ch -> ps ) e. _G ` for ` ch e. _G ` .  The present
+     theorem is then an element of ` _G ` , and the implications occurring in
+     the theorem are in one-to-one correspondence with the formulas in ` _G `
+     up to logical equivalence.  In particular, the theorem itself is
+     equivalent to ` T. e. _G ` .  (Contributed by Adrian Ducourtial,
+     2-Oct-2025.) $)
+  antnest $p |- ( ( ( ( ( ( T. -> ph ) -> ps ) -> ps ) -> ph ) -> ps ) -> ps )
+    $=
+    ( wtru wi wn simplim conax1 mtod syl syl11 mptru pm2.65i notnotri ) CADZBDZ
+    BDZADZBDZBDZSEZATADOECATNBFTOBRBGZTQEZPTQBUARBFHZPAFIHJKTUBAEUCPAGILM $.
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=