From 2142f9dfcf72f83046feebcda91be5817da17e10 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 10 Nov 2024 14:29:23 +0100 Subject: [PATCH] iset: fix typo in ~ifelpwund and ~ifexd. --- iset.mm | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/iset.mm b/iset.mm index 8ea2bec77d..49a5765f0f 100644 --- a/iset.mm +++ b/iset.mm @@ -39764,8 +39764,8 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ), ifelpwund.2 $e |- ( ph -> B e. W ) $. $( Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) $) - ifelpwund $p |- ( ph -> if ( ph , A , B ) e. ~P ( A u. B ) ) $= - ( wcel cif cun cpw ifelpwung syl2anc ) ABDHCEHABCIBCJKHFGABCDELM $. + ifelpwund $p |- ( ph -> if ( ps , A , B ) e. ~P ( A u. B ) ) $= + ( wcel cif cun cpw ifelpwung syl2anc ) ACEIDFIBCDJCDKLIGHBCDEFMN $. $} ${ @@ -39782,8 +39782,8 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ), ifexd.2 $e |- ( ph -> B e. W ) $. $( Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) $) - ifexd $p |- ( ph -> if ( ph , A , B ) e. _V ) $= - ( cif cun cpw ifelpwund elexd ) AABCHBCIJABCDEFGKL $. + ifexd $p |- ( ph -> if ( ps , A , B ) e. _V ) $= + ( cif cun cpw ifelpwund elexd ) ABCDICDJKABCDEFGHLM $. $}