Theorem bj-0 32533

Description: A syntactic theorem. See the section comment and the comment of bj-1 32534. The full proof (that is, with the syntactic, non-essential steps) does not appear on this webpage. It has five steps and reads $= wph wps wi wch wi $. The only other syntactic theorems in the main part of set.mm are wel 1991 and weq 1874. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
bj-0	wff ( ( ph -> ps ) -> ch )

Proof of Theorem bj-0

Step	Hyp	Ref	Expression
1		wi 4	1 wff ( ( ph -> ps ) -> ch )

Syntax hints:   -> wi 4

This theorem is referenced by:  bj-1  32534