Metamath Proof Explorer

Theorem sbrimvw

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim based on fewer axioms, but with more disjoint variable conditions. (Contributed by Wolf Lammen, 29-Jan-2024) Remove DV condition. (Revised by Wolf Lammen, 5-Jun-2026)

Ref Expression
Assertion sbrimvw 
|- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )

Proof

Step Hyp Ref Expression
1 sbv 
 |-  ( [ y / x ] ph <-> ph )
2 sbi1 
 |-  ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
3 1 2 biimtrrid 
 |-  ( [ y / x ] ( ph -> ps ) -> ( ph -> [ y / x ] ps ) )
4 sbv 
 |-  ( [ y / x ] -. ph <-> -. ph )
5 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
6 5 sbimi 
 |-  ( [ y / x ] -. ph -> [ y / x ] ( ph -> ps ) )
7 4 6 sylbir 
 |-  ( -. ph -> [ y / x ] ( ph -> ps ) )
8 ax-1 
 |-  ( ps -> ( ph -> ps ) )
9 8 sbimi 
 |-  ( [ y / x ] ps -> [ y / x ] ( ph -> ps ) )
10 7 9 ja 
 |-  ( ( ph -> [ y / x ] ps ) -> [ y / x ] ( ph -> ps ) )
11 3 10 impbii 
 |-  ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )