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