search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

disjunctive normal form for wl-df-3mintru2 #4045

Closed wlammen closed 3 months ago

wlammen commented 3 months ago
  1. Mathbox: delete some empty lines, fix a typo
  2. Mathbox: add a cador like definition alternative for wl-df-3mintru2
  3. Mathbox: utility theorem wl-ifpimpr providing a simpler expression for an if-condition, if one case is a consequence of the other
  4. Delete outdated OLD theorems