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

Revise cbvreuw #4474

Merged
merged 4 commits into from
Dec 11, 2024
Merged

Revise cbvreuw #4474

merged 4 commits into from
Dec 11, 2024

Conversation

wlammen
Copy link
Contributor

@wlammen wlammen commented Dec 10, 2024 •
edited
Loading

  1. shorten and revise the proof of cbvreuw. Does not depend on ax-10 anymore.
  2. Reduce the symbol count in cbvrexfw. This minor shortening spares two ¬ in the proof display. No OLD version for this trivial change-
  3. Clean up: Reorder some ralbid * v proofs right after ralimd * v ones. This follows the pattern used in predicate logic where albidv follows right after alimdv related stuff.

@wlammen wlammen changed the title Revise Revise cbvreuw Dec 10, 2024
icecream17
icecream17 approved these changes Dec 10, 2024
View reviewed changes
set.mm Show resolved Hide resolved
@wlammen wlammen merged commit 88304ba into metamath:develop Dec 11, 2024
10 checks passed
@wlammen wlammen deleted the wl-1 branch December 11, 2024 05:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@icecream17 icecream17 icecream17 approved these changes

@avekens avekens avekens approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@wlammen @avekens @icecream17