By our conventions,
*"A theorem is in "deduction form" (or is a "deduction") if it has one or more $e hypotheses, and the hypotheses and the conclusion are implications that share the same antecedent. More precisely, the conclusion is an implication with a wff variable as the antecedent (usually ` ph `), and every hypothesis ($e statement) is either: ..."* There are, however, some theorems of the form `ph -> xxx ` which have a label ending with "d", but are no "deductions" because they have no hypotheses, e.g. ~eqidd, ~biidd, ~exmidd, ~fvexd These theorems are only convenience theorems saving an ~a1i in the proofs(for example, ~eqidd is used 1441 times), but have no significant meaning, because they always say "something true follows from anything". Is it justified that such theorems have suffix "d" although they are no deductions? With a lot of good will, one can say that there is an implicit hypothesis `ph -> T. ` (which is always true, see ~a1tru) which would make these theorems deductions. Or would it be better to use a different suffix or a complete different naming convention for such theorems? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/54ca7750-1969-478a-bb18-121ff550e792n%40googlegroups.com.
