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

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 ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbv ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
2 sbi1 ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
3 1 2 biimtrrid ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
4 sbv ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜑 )
5 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
6 5 sbimi ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
7 4 6 sylbir ⊢ ( ¬ 𝜑 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
8 ax-1 ⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
9 8 sbimi ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
10 7 9 ja ⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) → [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) )
11 3 10 impbii ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )