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 44901
Description: Virtual deduction proof of 2pm13.193 44550. 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 44550 is 2pm13.193VD 44901 without virtual deductions and was automatically derived from 2pm13.193VD 44901. (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 44572 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
2 simpl 482 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
31, 2e1a 44625 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
4 simpl 482 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
53, 4e1a 44625 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑥 = 𝑢   )
6 simpr 484 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
71, 6e1a 44625 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
8 pm3.21 471 . . . . . . . . . 10 (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)))
95, 7, 8e11 44686 . . . . . . . . 9 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
10 sbequ2 2247 . . . . . . . . . 10 (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑣 / 𝑦]𝜑))
1110imdistanri 569 . . . . . . . . 9 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢) → ([𝑣 / 𝑦]𝜑𝑥 = 𝑢))
129, 11e1a 44625 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
13 simpl 482 . . . . . . . 8 (([𝑣 / 𝑦]𝜑𝑥 = 𝑢) → [𝑣 / 𝑦]𝜑)
1412, 13e1a 44625 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
15 simpr 484 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
163, 15e1a 44625 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝑦 = 𝑣   )
17 pm3.2 469 . . . . . . 7 ([𝑣 / 𝑦]𝜑 → (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)))
1814, 16, 17e11 44686 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
19 sbequ2 2247 . . . . . . 7 (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑𝜑))
2019imdistanri 569 . . . . . 6 (([𝑣 / 𝑦]𝜑𝑦 = 𝑣) → (𝜑𝑦 = 𝑣))
2118, 20e1a 44625 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   (𝜑𝑦 = 𝑣)   )
22 simpl 482 . . . . 5 ((𝜑𝑦 = 𝑣) → 𝜑)
2321, 22e1a 44625 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   𝜑   )
24 pm3.2 469 . . . 4 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
253, 23, 24e11 44686 . . 3 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
2625in1 44569 . 2 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
27 idn1 44572 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
28 simpl 482 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
2927, 28e1a 44625 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
3029, 4e1a 44625 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑥 = 𝑢   )
3129, 15e1a 44625 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝑦 = 𝑣   )
32 simpr 484 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → 𝜑)
3327, 32e1a 44625 . . . . . . . . . 10 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   𝜑   )
34 pm3.21 471 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝜑 → (𝜑𝑦 = 𝑣)))
3531, 33, 34e11 44686 . . . . . . . . 9 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   (𝜑𝑦 = 𝑣)   )
36 sbequ1 2246 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝜑 → [𝑣 / 𝑦]𝜑))
3736imdistanri 569 . . . . . . . . 9 ((𝜑𝑦 = 𝑣) → ([𝑣 / 𝑦]𝜑𝑦 = 𝑣))
3835, 37e1a 44625 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑦 = 𝑣)   )
39 simpl 482 . . . . . . . 8 (([𝑣 / 𝑦]𝜑𝑦 = 𝑣) → [𝑣 / 𝑦]𝜑)
4038, 39e1a 44625 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑣 / 𝑦]𝜑   )
41 pm3.21 471 . . . . . . 7 (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)))
4230, 40, 41e11 44686 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
43 sbequ1 2246 . . . . . . 7 (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
4443imdistanri 569 . . . . . 6 (([𝑣 / 𝑦]𝜑𝑥 = 𝑢) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢))
4542, 44e1a 44625 . . . . 5 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢)   )
46 simpl 482 . . . . 5 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑𝑥 = 𝑢) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
4745, 46e1a 44625 . . . 4 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
48 pm3.2 469 . . . 4 ((𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
4929, 47, 48e11 44686 . . 3 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
5049in1 44569 . 2 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
5126, 50impbii 209 1 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  [wsb 2062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-vd1 44568
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator