Metamath Proof Explorer

Theorem 2pm13.193

Description: pm13.193 for two variables. pm13.193 is Theorem *13.193 in WhiteheadRussell p. 179. Derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	2pm13.193	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow ((x = u \land y = v) \land φ)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to x = u$
2		simplr	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to y = v$
3		simpr	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to [u/ x] [v/ y] φ$
4		sbequ2	$⊢ x = u \to ([u/ x] [v/ y] φ \to [v/ y] φ)$
5	1 3 4	sylc	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to [v/ y] φ$
6		sbequ2	$⊢ y = v \to ([v/ y] φ \to φ)$
7	2 5 6	sylc	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to φ$
8	1 2 7	jca31	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \to ((x = u \land y = v) \land φ)$
9		simpll	$⊢ ((x = u \land y = v) \land φ) \to x = u$
10		simplr	$⊢ ((x = u \land y = v) \land φ) \to y = v$
11		simpr	$⊢ ((x = u \land y = v) \land φ) \to φ$
12		sbequ1	$⊢ y = v \to (φ \to [v/ y] φ)$
13	10 11 12	sylc	$⊢ ((x = u \land y = v) \land φ) \to [v/ y] φ$
14		sbequ1	$⊢ x = u \to ([v/ y] φ \to [u/ x] [v/ y] φ)$
15	9 13 14	sylc	$⊢ ((x = u \land y = v) \land φ) \to [u/ x] [v/ y] φ$
16	9 10 15	jca31	$⊢ ((x = u \land y = v) \land φ) \to ((x = u \land y = v) \land [u/ x] [v/ y] φ)$
17	8 16	impbii	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow ((x = u \land y = v) \land φ)$