Theorem bj-0 31703

Description: A syntactic theorem. See the section comment and the comment of bj-1 31704. 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 1978 and weq 1861. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
bj-0	wff ((𝜑 → 𝜓) → 𝜒)

Proof of Theorem bj-0

Step	Hyp	Ref	Expression
1		wi 4	1 wff ((𝜑 → 𝜓) → 𝜒)

Syntax hints:   → wi 4

This theorem is referenced by:  bj-1  31704