This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbbii

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993)

		Ref	Expression
	Hypothesis	sbbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	sbbii	$⊢ [t/ x] φ \leftrightarrow [t/ x] ψ$

Step	Hyp	Ref	Expression
1		sbbii.1	$⊢ φ \leftrightarrow ψ$
2	1	biimpi	$⊢ φ \to ψ$
3	2	sbimi	$⊢ [t/ x] φ \to [t/ x] ψ$
4	1	biimpri	$⊢ ψ \to φ$
5	4	sbimi	$⊢ [t/ x] ψ \to [t/ x] φ$
6	3 5	impbii	$⊢ [t/ x] φ \leftrightarrow [t/ x] ψ$