Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

shorten nfnbi #4268

Merged
merged 2 commits into from
Oct 6, 2024
Merged

shorten nfnbi #4268

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4c86876
shorten nfnbi
wlammen Oct 6, 2024
dd50087
fix line break in wrong place
wlammen Oct 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 4 additions & 8 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,6 @@
"2ax6e" is used by "2sb5rf".
"2ax6e" is used by "2sb6rf".
"2ax6elem" is used by "2ax6e".
"2ax6elem" is used by "2ax6eOLD".
"2eu1" is used by "2eu2".
"2eu1" is used by "2eu3".
"2eu2" is used by "2eu8".
Expand Down Expand Up @@ -3200,7 +3199,6 @@
"cbvexd" is used by "axunnd".
"cbvexd" is used by "cbvexdva".
"cbvexd" is used by "dfid3".
"cbvexd" is used by "vtoclgftOLD".
"cbvexd" is used by "wl-eudf".
"cbvexd" is used by "wl-mo2df".
"cbvexdva" is used by "cbvex2vv".
Expand Down Expand Up @@ -13837,8 +13835,7 @@ New usage of "235t711" is discouraged (0 uses).
New usage of "2atm2atN" is discouraged (0 uses).
New usage of "2atnelvolN" is discouraged (0 uses).
New usage of "2ax6e" is discouraged (2 uses).
New usage of "2ax6eOLD" is discouraged (0 uses).
New usage of "2ax6elem" is discouraged (2 uses).
New usage of "2ax6elem" is discouraged (1 uses).
New usage of "2bornot2b" is discouraged (0 uses).
New usage of "2cnALT" is discouraged (0 uses).
New usage of "2eu1" is discouraged (2 uses).
Expand Down Expand Up @@ -14839,7 +14836,7 @@ New usage of "cbvex" is discouraged (3 uses).
New usage of "cbvex2" is discouraged (0 uses).
New usage of "cbvex2vv" is discouraged (1 uses).
New usage of "cbvex4v" is discouraged (0 uses).
New usage of "cbvexd" is discouraged (12 uses).
New usage of "cbvexd" is discouraged (11 uses).
New usage of "cbvexdva" is discouraged (1 uses).
New usage of "cbvexsv" is discouraged (2 uses).
New usage of "cbvexv" is discouraged (1 uses).
Expand Down Expand Up @@ -17348,6 +17345,7 @@ New usage of "nfmod" is discouraged (2 uses).
New usage of "nfmod2" is discouraged (5 uses).
New usage of "nfnae" is discouraged (43 uses).
New usage of "nfnaewOLD" is discouraged (0 uses).
New usage of "nfnbiOLD" is discouraged (0 uses).
New usage of "nfopdALT" is discouraged (0 uses).
New usage of "nfra2" is discouraged (1 uses).
New usage of "nfra2wOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -18750,7 +18748,6 @@ New usage of "vtocl3gaOLD" is discouraged (0 uses).
New usage of "vtoclALT" is discouraged (0 uses).
New usage of "vtocldOLD" is discouraged (0 uses).
New usage of "vtoclgOLD" is discouraged (0 uses).
New usage of "vtoclgftOLD" is discouraged (0 uses).
New usage of "vtxdusgr0edgnelALT" is discouraged (0 uses).
New usage of "w-bnj13" is discouraged (5 uses).
New usage of "w-bnj15" is discouraged (92 uses).
Expand Down Expand Up @@ -18848,7 +18845,6 @@ Proof modification of "1oexOLD" is discouraged (4 steps).
Proof modification of "1p1e2apr1" is discouraged (7 steps).
Proof modification of "1p2e3ALT" is discouraged (7 steps).
Proof modification of "1t1e1ALT" is discouraged (13 steps).
Proof modification of "2ax6eOLD" is discouraged (47 steps).
Proof modification of "2bornot2b" is discouraged (26 steps).
Proof modification of "2cnALT" is discouraged (3 steps).
Proof modification of "2falsedOLD" is discouraged (14 steps).
Expand Down Expand Up @@ -20021,6 +20017,7 @@ Proof modification of "nfcriiOLD" is discouraged (40 steps).
Proof modification of "nfequid-o" is discouraged (8 steps).
Proof modification of "nfeu1ALT" is discouraged (25 steps).
Proof modification of "nfnaewOLD" is discouraged (14 steps).
Proof modification of "nfnbiOLD" is discouraged (46 steps).
Proof modification of "nfopdALT" is discouraged (70 steps).
Proof modification of "nfra2wOLD" is discouraged (15 steps).
Proof modification of "nfraldwOLD" is discouraged (41 steps).
Expand Down Expand Up @@ -20458,7 +20455,6 @@ Proof modification of "vtocl3gaOLD" is discouraged (45 steps).
Proof modification of "vtoclALT" is discouraged (11 steps).
Proof modification of "vtocldOLD" is discouraged (21 steps).
Proof modification of "vtoclgOLD" is discouraged (11 steps).
Proof modification of "vtoclgftOLD" is discouraged (142 steps).
Proof modification of "vtxdusgr0edgnelALT" is discouraged (94 steps).
Proof modification of "wl-cases2-dnf" is discouraged (85 steps).
Proof modification of "wl-dfclab" is discouraged (73 steps).
Expand Down
31 changes: 9 additions & 22 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15273,8 +15273,16 @@ only postulated (that is, axiomatic) rule of inference of predicate
$}

$( A variable is nonfree in a proposition if and only if it is so in its
negation. (Contributed by BJ, 6-May-2019.) $)
negation. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf
Lammen, 6-Oct-2024.) $)
nfnbi $p |- ( F/ x ph <-> F/ x -. ph ) $=
( wn wex wal wi wnf exnal imbi1i df-nf nf4 3bitr4ri ) ACZBDZMBEZFABECZOFMBG
ABGNPOABHIMBJABKL $.

$( Obsolete version of ~ nfnbi as of 6-Oct-2024. (Contributed by BJ,
6-May-2019.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
nfnbiOLD $p |- ( F/ x ph <-> F/ x -. ph ) $=
( wal wn wo wnf orcom nf3 notnotb albii orbi2i bitr4i 3bitr4i ) ABCZADZBCZE
PNEZABFOBFZNPGABHRPODZBCZEQOBHNTPASBAIJKLM $.

Expand Down Expand Up @@ -21698,13 +21706,6 @@ nonfreeness hypothesis ( ~ equs45f ). Usage of this theorem is
2ax6e $p |- E. z E. w ( z = x /\ w = y ) $=
( weq wal wa wex aeveq jca 19.8ad 2ax6elem pm2.61i ) DCEDFZCAEZDBEZGZDHZC
HNRCNQDNOPDCCAIDCDBIJKKABCDLM $.

$( Obsolete version of ~ 2ax6e as of 3-Oct-2023. (Contributed by Wolf
Lammen, 28-Sep-2018.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
2ax6eOLD $p |- E. z E. w ( z = x /\ w = y ) $=
( weq wal wa wex aeveq jca 19.8a 3syl 2ax6elem pm2.61i ) DCEDFZCAEZDBEZGZ
DHZCHZORSTOPQDCCAIDCDBIJRDKSCKLABCDMN $.
$}

${
Expand Down Expand Up @@ -32280,20 +32281,6 @@ general is seen either by substitution (when the variable ` V ` has no
CFOWNVMWOWHWFKCFURWQWFWHUSUTQVAWDFRVQCRVBVCSVDVEVOVTWBBKZWAVOVTWRVTVQBKZC
LZVOWRVSAWSCVSAWSVSVQABVRABKVQABPVGVFTVHVNWTWRJVMVQBCVIVJSTVKVL $.
$( $j usage 'vtoclgft' avoids 'ax-13'; $)

$( Obsolete version of ~ vtoclgft as of 6-Oct-2023. (Contributed by NM,
17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof
shortened by JJ, 11-Aug-2021.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
vtoclgftOLD $p |- ( ( ( F/_ x A /\ F/ x ps )
/\ ( A. x ( x = A -> ( ph <-> ps ) )
/\ A. x ph ) /\ A e. V ) -> ps ) $=
( vz wnfc wnf wa cv wceq wb wi wal wcel w3a wex elisset syl5ib imp nfnfc1
nfcvd id nfeqd weq eqeq1 cbvexd ad2antrr 3impia biimp imim2i com23 19.23t
a1i alanimi adantl 3adant3 mpd ) CDGZBCHZIZCJZDKZABLZMZCNACNIZDEOZPVCCQZB
VAVFVGVHUSVGVHMUTVFVGFJZDKZFQUSVHFDERUSVJVCFCCDUAUSCVIDUSCVIUBUSUCUDFCUEV
JVCLMUSVIVBDUFUNUGSUHUIVAVFVHBMZVGVAVFVKVFVCBMZCNZVAVKVEAVLCVEAVLVEVCABVD
ABMVCABUJUKULTUOUTVMVKLUSVCBCUMUPSTUQUR $.
$}

${
Expand Down
Loading