Nested antecedents (#5033)

* Basic clone theory in AD's mathbox

* Change label and description of df-superpos

* Clarify description of df-suppos

* Add display info and distinct variable conditions

* Elaborate citations

* Adjust rewrapping

* Add space

* Nested antecedents

* Rewrapping

---------

Co-authored-by: Adrian Ducourtial <[email protected]>

Author: ducourtial

set.mm

@@ -571203,6 +571203,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 $.
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=