Theorem sbrim

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) Avoid ax-10 . (Revised by Gino Giotto, 20-Nov-2024)

	Ref	Expression
Hypothesis	sbrim.1	|- F/ x ph
Assertion	sbrim	|- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbrim.1	|- F/ x ph
2		bi2.04	|- ( ( x = t -> ( ph -> ps ) ) <-> ( ph -> ( x = t -> ps ) ) )
3	2	albii	|- ( A. x ( x = t -> ( ph -> ps ) ) <-> A. x ( ph -> ( x = t -> ps ) ) )
4	1	19.21	|- ( A. x ( ph -> ( x = t -> ps ) ) <-> ( ph -> A. x ( x = t -> ps ) ) )
5	3 4	bitri	|- ( A. x ( x = t -> ( ph -> ps ) ) <-> ( ph -> A. x ( x = t -> ps ) ) )
6	5	imbi2i	|- ( ( t = y -> A. x ( x = t -> ( ph -> ps ) ) ) <-> ( t = y -> ( ph -> A. x ( x = t -> ps ) ) ) )
7		bi2.04	|- ( ( t = y -> ( ph -> A. x ( x = t -> ps ) ) ) <-> ( ph -> ( t = y -> A. x ( x = t -> ps ) ) ) )
8	6 7	bitri	|- ( ( t = y -> A. x ( x = t -> ( ph -> ps ) ) ) <-> ( ph -> ( t = y -> A. x ( x = t -> ps ) ) ) )
9	8	albii	|- ( A. t ( t = y -> A. x ( x = t -> ( ph -> ps ) ) ) <-> A. t ( ph -> ( t = y -> A. x ( x = t -> ps ) ) ) )
10		df-sb	|- ( [ y / x ] ( ph -> ps ) <-> A. t ( t = y -> A. x ( x = t -> ( ph -> ps ) ) ) )
11		df-sb	|- ( [ y / x ] ps <-> A. t ( t = y -> A. x ( x = t -> ps ) ) )
12	11	imbi2i	|- ( ( ph -> [ y / x ] ps ) <-> ( ph -> A. t ( t = y -> A. x ( x = t -> ps ) ) ) )
13		19.21v	|- ( A. t ( ph -> ( t = y -> A. x ( x = t -> ps ) ) ) <-> ( ph -> A. t ( t = y -> A. x ( x = t -> ps ) ) ) )
14	12 13	bitr4i	|- ( ( ph -> [ y / x ] ps ) <-> A. t ( ph -> ( t = y -> A. x ( x = t -> ps ) ) ) )
15	9 10 14	3bitr4i	|- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )