Metamath Proof Explorer


Theorem bj-0

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 )