Theorem bj-1

Description: In this proof, the use of the syntactic theorem bj-0 allows to reduce the total length by one (non-essential) step. See also the section comment and the comment of bj-0 . Since bj-0 is used in a non-essential step, this use does not appear on this webpage (but the present theorem appears on the webpage for bj-0 as a theorem referencing it). The full proof reads $= wph wps wch bj-0 id $. (while, without using bj-0 , it would read $= wph wps wi wch wi id $.).

Now we explain why syntactic theorems are not useful in set.mm. Suppose that the syntactic theorem thm-0 proves that PHI is a well-formed formula, and that thm-0 is used to shorten the proof of thm-1. Assume that PHI does have proper non-atomic subformulas (which is not the case of the formula proved by weq or wel ). Then, the proof of thm-1 does not construct all the proper non-atomic subformulas of PHI (if it did, then using thm-0 would not shorten it). Therefore, thm-1 is a special instance of a more general theorem with essentially the same proof. In the present case, bj-1 is a special instance of id . (Contributed by BJ, 24-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-1	|- ( ( ( ph -> ps ) -> ch ) -> ( ( ph -> ps ) -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( ( ph -> ps ) -> ch ) -> ( ( ph -> ps ) -> ch ) )