Skip to content

Commit

Permalink
iset: fix typo in ~ifelpwund and ~ifexd.
Browse files Browse the repository at this point in the history
  • Loading branch information
benjub committed Nov 10, 2024
1 parent 0e1c00e commit 2142f9d
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions iset.mm
Original file line number Diff line number Diff line change
Expand Up @@ -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 $.
$}

${
Expand All @@ -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 $.
$}


Expand Down

0 comments on commit 2142f9d

Please sign in to comment.