Theorem sbcimi

Description: Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypotheses	sbcimi.1	|- A e. _V
	sbcimi.2	|- ( [. A / x ]. ph <-> ch )
	sbcimi.3	|- ( [. A / x ]. ps <-> et )
Assertion	sbcimi	|- ( [. A / x ]. ( ph -> ps ) <-> ( ch -> et ) )

Proof

Step	Hyp	Ref	Expression
1		sbcimi.1	|- A e. _V
2		sbcimi.2	|- ( [. A / x ]. ph <-> ch )
3		sbcimi.3	|- ( [. A / x ]. ps <-> et )
4		sbcimg	|- ( A e. _V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
5	1 4	ax-mp	|- ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) )
6	2 3	imbi12i	|- ( ( [. A / x ]. ph -> [. A / x ]. ps ) <-> ( ch -> et ) )
7	5 6	bitri	|- ( [. A / x ]. ( ph -> ps ) <-> ( ch -> et ) )