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	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → 𝑥 = 𝑢 )
2		simplr	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑣 )
3		simpr	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
4		sbequ2	⊢ ( 𝑥 = 𝑢 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑣 / 𝑦 ] 𝜑 ) )
5	1 3 4	sylc	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → [ 𝑣 / 𝑦 ] 𝜑 )
6		sbequ2	⊢ ( 𝑦 = 𝑣 → ( [ 𝑣 / 𝑦 ] 𝜑 → 𝜑 ) )
7	2 5 6	sylc	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → 𝜑 )
8	1 2 7	jca31	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
9		simpll	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → 𝑥 = 𝑢 )
10		simplr	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → 𝑦 = 𝑣 )
11		simpr	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → 𝜑 )
12		sbequ1	⊢ ( 𝑦 = 𝑣 → ( 𝜑 → [ 𝑣 / 𝑦 ] 𝜑 ) )
13	10 11 12	sylc	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → [ 𝑣 / 𝑦 ] 𝜑 )
14		sbequ1	⊢ ( 𝑥 = 𝑢 → ( [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
15	9 13 14	sylc	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
16	9 10 15	jca31	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
17	8 16	impbii	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )