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

Metamath Proof Explorer

Theorem sbc19.21g

Description: Substitution for a variable not free in antecedent affects only the consequent. (Contributed by NM, 11-Oct-2004)

Ref Expression
Hypothesis sbcgf.1 
|- F/ x ph
Assertion sbc19.21g 
|- ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( ph -> [. A / x ]. ps ) ) )

Proof

Step Hyp Ref Expression
1 sbcgf.1 
 |-  F/ x ph
2 sbcimg 
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
3 1 sbcgf 
 |-  ( A e. V -> ( [. A / x ]. ph <-> ph ) )
4 3 imbi1d 
 |-  ( A e. V -> ( ( [. A / x ]. ph -> [. A / x ]. ps ) <-> ( ph -> [. A / x ]. ps ) ) )
5 2 4 bitrd 
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( ph -> [. A / x ]. ps ) ) )