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

Metamath Proof Explorer

Theorem sbievw2

Description: sbievw applied twice, avoiding a DV condition on x , y . Based on proofs by Wolf Lammen. (Contributed by Steven Nguyen, 29-Jul-2023)

Ref Expression
Hypotheses sbievw2.1 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
sbievw2.2 ⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
Assertion sbievw2 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 sbievw2.1 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
2 sbievw2.2 ⊢ ( 𝑤 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
3 sbcom3vv ⊢ ( [ 𝑦 / 𝑤 ] [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 )
4 1 sbievw ⊢ ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜒 )
5 4 sbbii ⊢ ( [ 𝑦 / 𝑤 ] [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑤 ] 𝜒 )
6 sbv ⊢ ( [ 𝑦 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
7 3 5 6 3bitr3i ⊢ ( [ 𝑦 / 𝑤 ] 𝜒 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
8 2 sbievw ⊢ ( [ 𝑦 / 𝑤 ] 𝜒 ↔ 𝜓 )
9 7 8 bitr3i ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )