Metamath Proof Explorer

Theorem spsbbi

Description: Biconditional property for substitution. Closed form of sbbii . Specialization of biconditional. (Contributed by NM, 2-Jun-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

		Ref	Expression
	Assertion	spsbbi	$⊢ \forall x (φ \leftrightarrow ψ) \to ([t/ x] φ \leftrightarrow [t/ x] ψ)$

Proof

Step	Hyp	Ref	Expression
1		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
2	1	alimi	$⊢ \forall x (φ \leftrightarrow ψ) \to \forall x (φ \to ψ)$
3		spsbim	$⊢ \forall x (φ \to ψ) \to ([t/ x] φ \to [t/ x] ψ)$
4	2 3	syl	$⊢ \forall x (φ \leftrightarrow ψ) \to ([t/ x] φ \to [t/ x] ψ)$
5		biimpr	$⊢ (φ \leftrightarrow ψ) \to (ψ \to φ)$
6	5	alimi	$⊢ \forall x (φ \leftrightarrow ψ) \to \forall x (ψ \to φ)$
7		spsbim	$⊢ \forall x (ψ \to φ) \to ([t/ x] ψ \to [t/ x] φ)$
8	6 7	syl	$⊢ \forall x (φ \leftrightarrow ψ) \to ([t/ x] ψ \to [t/ x] φ)$
9	4 8	impbid	$⊢ \forall x (φ \leftrightarrow ψ) \to ([t/ x] φ \leftrightarrow [t/ x] ψ)$