Theorem wl-2spsbbi

Description: spsbbi applied twice. (Contributed by Wolf Lammen, 5-Aug-2023)

	Ref	Expression
Assertion	wl-2spsbbi	⊢ ( ∀ 𝑎 ∀ 𝑏 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑎 ∀ 𝑏 ( 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑏 ∀ 𝑎 ( 𝜑 ↔ 𝜓 ) )
2		nfa1	⊢ Ⅎ 𝑏 ∀ 𝑏 ∀ 𝑎 ( 𝜑 ↔ 𝜓 )
3		nfa1	⊢ Ⅎ 𝑎 ∀ 𝑎 ( 𝜑 ↔ 𝜓 )
4		sp	⊢ ( ∀ 𝑎 ( 𝜑 ↔ 𝜓 ) → ( 𝜑 ↔ 𝜓 ) )
5	3 4	sbbid	⊢ ( ∀ 𝑎 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜓 ) )
6	5	sps	⊢ ( ∀ 𝑏 ∀ 𝑎 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜓 ) )
7	2 6	sbbid	⊢ ( ∀ 𝑏 ∀ 𝑎 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜓 ) )
8	1 7	sylbi	⊢ ( ∀ 𝑎 ∀ 𝑏 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜓 ) )