Theorem sbievw2

Description: sbievw applied twice, avoiding a DV condition on x , y . Based on proofs by Wolf Lammen. (Contributed by Steven Nguyen, 29-Jul-2023)

	Ref	Expression
Hypotheses	sbievw2.1	|- ( x = w -> ( ph <-> ch ) )
	sbievw2.2	|- ( w = y -> ( ch <-> ps ) )
Assertion	sbievw2	|- ( [ y / x ] ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		sbievw2.1	|- ( x = w -> ( ph <-> ch ) )
2		sbievw2.2	|- ( w = y -> ( ch <-> ps ) )
3		sbcom3vv	|- ( [ y / w ] [ w / x ] ph <-> [ y / w ] [ y / x ] ph )
4	1	sbievw	|- ( [ w / x ] ph <-> ch )
5	4	sbbii	|- ( [ y / w ] [ w / x ] ph <-> [ y / w ] ch )
6		sbv	|- ( [ y / w ] [ y / x ] ph <-> [ y / x ] ph )
7	3 5 6	3bitr3i	|- ( [ y / w ] ch <-> [ y / x ] ph )
8	2	sbievw	|- ( [ y / w ] ch <-> ps )
9	7 8	bitr3i	|- ( [ y / x ] ph <-> ps )