Theorem sblbis

Description: Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993)

	Ref	Expression
Hypothesis	sblbis.1	|- ( [ y / x ] ph <-> ps )
Assertion	sblbis	|- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		sblbis.1	|- ( [ y / x ] ph <-> ps )
2		sbbi	|- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> [ y / x ] ph ) )
3	1	bibi2i	|- ( ( [ y / x ] ch <-> [ y / x ] ph ) <-> ( [ y / x ] ch <-> ps ) )
4	2 3	bitri	|- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) )