Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2pm13.193VD Structured version   Visualization version   GIF version

Theorem 2pm13.193VD 42852
Description: Virtual deduction proof of 2pm13.193 42501. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 2pm13.193 42501 is 2pm13.193VD 42852 without virtual deductions and was automatically derived from 2pm13.193VD 42852. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
2:1: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
3:2: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   𝑥 = 𝑢   )
4:1: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
5:3,4: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
6:5: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
7:6: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
8:2: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   𝑦 = 𝑣   )
9:7,8: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
10:9: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   (𝜑𝑦 = 𝑣)   )
11:10: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   𝜑   )
12:2,11: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
13:12: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
14:: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (( 𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
15:14: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
16:15: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑦 = 𝑣   )
17:14: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝜑    )
18:16,17: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ( 𝜑𝑦 = 𝑣)   )
19:18: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([ 𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
20:15: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑥 = 𝑢   )
21:19: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
22:20,21: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([ 𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
23:22: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
24:23: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
25:15,24: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (( 𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
26:25: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
qed:13,26: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
Assertion
Ref Expression
2pm13.193VD (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))

Proof of Theorem 2pm13.193VD
StepHypRef Expression
1 idn1 42523 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
2 simpl 483 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
31, 2e1a 42576 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
4 simpl 483 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
53, 4e1a 42576 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑥 = 𝑢   )
6 simpr 485 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
71, 6e1a 42576 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
8 pm3.21 472 . . . . . . . . . 10 (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)))
95, 7, 8e11 42637 . . . . . . . . 9 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
10 sbequ2 2240 . . . . . . . . . 10 (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑣 / 𝑦]𝜑))
1110imdistanri 570 . . . . . . . . 9 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢) → ([𝑣 / 𝑦]𝜑𝑥 = 𝑢))
129, 11e1a 42576 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
13 simpl 483 . . . . . . . 8 (([𝑣 / 𝑦]𝜑𝑥 = 𝑢) → [𝑣 / 𝑦]𝜑)
1412, 13e1a 42576 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
15 simpr 485 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
163, 15e1a 42576 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑦 = 𝑣   )
17 pm3.2 470 . . . . . . 7 ([𝑣 / 𝑦]𝜑 → (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)))
1814, 16, 17e11 42637 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
19 sbequ2 2240 . . . . . . 7 (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑𝜑))
2019imdistanri 570 . . . . . 6 (([𝑣 / 𝑦]𝜑𝑦 = 𝑣) → (𝜑𝑦 = 𝑣))
2118, 20e1a 42576 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝜑𝑦 = 𝑣)   )
22 simpl 483 . . . . 5 ((𝜑𝑦 = 𝑣) → 𝜑)
2321, 22e1a 42576 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝜑   )
24 pm3.2 470 . . . 4 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
253, 23, 24e11 42637 . . 3 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
2625in1 42520 . 2 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
27 idn1 42523 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
28 simpl 483 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
2927, 28e1a 42576 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
3029, 4e1a 42576 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑥 = 𝑢   )
3129, 15e1a 42576 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑦 = 𝑣   )
32 simpr 485 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → 𝜑)
3327, 32e1a 42576 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝜑   )
34 pm3.21 472 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝜑 → (𝜑𝑦 = 𝑣)))
3531, 33, 34e11 42637 . . . . . . . . 9 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝜑𝑦 = 𝑣)   )
36 sbequ1 2239 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝜑 → [𝑣 / 𝑦]𝜑))
3736imdistanri 570 . . . . . . . . 9 ((𝜑𝑦 = 𝑣) → ([𝑣 / 𝑦]𝜑𝑦 = 𝑣))
3835, 37e1a 42576 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
39 simpl 483 . . . . . . . 8 (([𝑣 / 𝑦]𝜑𝑦 = 𝑣) → [𝑣 / 𝑦]𝜑)
4038, 39e1a 42576 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
41 pm3.21 472 . . . . . . 7 (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)))
4230, 40, 41e11 42637 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
43 sbequ1 2239 . . . . . . 7 (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
4443imdistanri 570 . . . . . 6 (([𝑣 / 𝑦]𝜑𝑥 = 𝑢) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢))
4542, 44e1a 42576 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
46 simpl 483 . . . . 5 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
4745, 46e1a 42576 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
48 pm3.2 470 . . . 4 ((𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
4929, 47, 48e11 42637 . . 3 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
5049in1 42520 . 2 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
5126, 50impbii 208 1 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1540  [wsb 2066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-12 2170
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-vd1 42519
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator