Theorem sbbii

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

	Ref	Expression
Hypothesis	sbbii.1	|- ( ph <-> ps )
Assertion	sbbii	|- ( [ t / x ] ph <-> [ t / x ] ps )

Proof

Step	Hyp	Ref	Expression
1		sbbii.1	|- ( ph <-> ps )
2	1	biimpi	|- ( ph -> ps )
3	2	sbimi	|- ( [ t / x ] ph -> [ t / x ] ps )
4	1	biimpri	|- ( ps -> ph )
5	4	sbimi	|- ( [ t / x ] ps -> [ t / x ] ph )
6	3 5	impbii	|- ( [ t / x ] ph <-> [ t / x ] ps )