Theorem sbbii

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993)

	Ref	Expression
Hypothesis	sbbii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	sbbii	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2	1	biimpi	⊢ ( 𝜑 → 𝜓 )
3	2	sbimi	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] 𝜓 )
4	1	biimpri	⊢ ( 𝜓 → 𝜑 )
5	4	sbimi	⊢ ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜑 )
6	3 5	impbii	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] 𝜓 )