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

Metamath Proof Explorer

Theorem 2sbievw

Description: Conversion of double implicit substitution to explicit substitution. Version of 2sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by AV, 29-Jul-2023) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

		Ref	Expression
	Hypothesis	2sbievw.1	$⊢ (x = t \land y = u) \to (φ \leftrightarrow ψ)$
	Assertion	2sbievw	$⊢ [t/ x] [u/ y] φ \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		2sbievw.1	$⊢ (x = t \land y = u) \to (φ \leftrightarrow ψ)$
2	1	sbiedvw	$⊢ x = t \to ([u/ y] φ \leftrightarrow ψ)$
3	2	sbievw	$⊢ [t/ x] [u/ y] φ \leftrightarrow ψ$