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\to \left(\phi \leftrightarrow \chi \right)$$
	sbievw2.2	$$⊢w=y\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	sbievw2	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		sbievw2.1	$$⊢x=w\to \left(\phi \leftrightarrow \chi \right)$$
2		sbievw2.2	$$⊢w=y\to \left(\chi \leftrightarrow \psi \right)$$
3		sbcom3vv	$$⊢\left[y/w\right]\left[w/x\right]\phi \leftrightarrow \left[y/w\right]\left[y/x\right]\phi$$
4	1	sbievw	$$⊢\left[w/x\right]\phi \leftrightarrow \chi$$
5	4	sbbii	$$⊢\left[y/w\right]\left[w/x\right]\phi \leftrightarrow \left[y/w\right]\chi$$
6		sbv	$$⊢\left[y/w\right]\left[y/x\right]\phi \leftrightarrow \left[y/x\right]\phi$$
7	3 5 6	3bitr3i	$$⊢\left[y/w\right]\chi \leftrightarrow \left[y/x\right]\phi$$
8	2	sbievw	$$⊢\left[y/w\right]\chi \leftrightarrow \psi$$
9	7 8	bitr3i	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$