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

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

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