Theorem sbrbis

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

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

Proof

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