Skip to content

Commit

Permalink
typo
Browse files Browse the repository at this point in the history
  • Loading branch information
wlammen committed Jan 28, 2024
1 parent 360dc36 commit 0702ee9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -22035,7 +22035,7 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
$d x y ps $. $d t y $.
2sbiev.1 $e |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) $.
$( Conversion of double implicit substitution to explicit substitution.
See ~ 2sbievw for variant with extra disjoint variables, but based on
See ~ 2sbievw for a variant with extra disjoint variables, but based on
fewer axioms. (Contributed by AV, 29-Jul-2023.) $)
2sbiev $p |- ( [ t / x ] [ u / y ] ph <-> ps ) $=
( wsb nfv weq sbiedv sbie ) ADEHBCFBCICFJABDEGKL $.
Expand Down

0 comments on commit 0702ee9

Please sign in to comment.