Theorem sbbi

Description: Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993)

	Ref	Expression
Assertion	sbbi	|- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		dfbi2	|- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
2	1	sbbii	|- ( [ y / x ] ( ph <-> ps ) <-> [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3		sbim	|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
4		sbim	|- ( [ y / x ] ( ps -> ph ) <-> ( [ y / x ] ps -> [ y / x ] ph ) )
5	3 4	anbi12i	|- ( ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ( ps -> ph ) ) <-> ( ( [ y / x ] ph -> [ y / x ] ps ) /\ ( [ y / x ] ps -> [ y / x ] ph ) ) )
6		sban	|- ( [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ( ps -> ph ) ) )
7		dfbi2	|- ( ( [ y / x ] ph <-> [ y / x ] ps ) <-> ( ( [ y / x ] ph -> [ y / x ] ps ) /\ ( [ y / x ] ps -> [ y / x ] ph ) ) )
8	5 6 7	3bitr4i	|- ( [ y / x ] ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )
9	2 8	bitri	|- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )