Description: A syntactic theorem. See the section comment and the comment of bj-1 . 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 and weq . (Contributed by BJ, 24-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-0 | wff ( ( ph -> ps ) -> ch ) |