ph |- ph is not an axiom by your definition, as it has the $e statement ph. >
Here "|-" is used loosely to separate the stack and the main statement. It belongs to a $e statement. It is meaningful in a formalism where the stack is appended to the left of the main statement. In full it would be: hp $a [ Ga , ph ] |- ph To separate $e statements and $p statements, I think metamath people use "&" and "=>". Look at the theorems page for instances of this convention. -- FL -- 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/47a6f583-8ee6-4de3-8299-7a8dd942438f%40googlegroups.com.
