This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 GG, 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 dfsb 
 |-  ( [ y / x ] ( ph -> ps ) <-> A. t ( t = y -> A. x ( x = t -> ( ph -> ps ) ) ) )
11 dfsb 
 |-  ( [ 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 ) )