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

Theorem 2uasbanhVD 41122
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 40780) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 40772 is 2uasbanhVD 41122 without virtual deductions and was automatically derived from 2uasbanhVD 41122. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
h1:: (𝜒 ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
100:1: (𝜒 → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
2:100: (   𝜒   ▶   (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
3:2: (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
4:3: (   𝜒   ▶   𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣 )   )
5:4: (   𝜒   ▶   (¬ ∀𝑥𝑥 = 𝑦𝑢 = 𝑣)    )
6:5: (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))   )
7:3,6: (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
8:2: (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
9:5: (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
10:8,9: (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜓   )
101:: ([𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
102:101: ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
103:: ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦 ]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
104:102,103: ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
11:7,10,104: (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦](𝜑 𝜓)   )
110:5: (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))   )
12:11,110: (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
120:12: (𝜒 → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣 ) ∧ (𝜑𝜓)))
13:1,120: ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → 𝑥𝑦((𝑥 = 𝑢 𝑦 = 𝑣) ∧ (𝜑𝜓)))
14:: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
15:14: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
16:14: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   (𝜑𝜓)   )
17:16: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   𝜑   )
18:15,17: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
19:18: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 )) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
20:19: (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑 𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
21:20: (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
22:16: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   𝜓   )
23:15,22: (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 ))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
24:23: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓 )) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
25:24: (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑 𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
26:25: (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
27:21,26: (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝜑𝜓)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ 𝑥𝑦( (𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
qed:13,27: (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝜑𝜓)) ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ 𝑥𝑦( (𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Hypothesis
Ref Expression
2uasbanhVD.1 (𝜒 ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Assertion
Ref Expression
2uasbanhVD (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣,𝑢)   𝜓(𝑥,𝑦,𝑣,𝑢)   𝜒(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem 2uasbanhVD
StepHypRef Expression
1 idn1 40785 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
2 simpl 483 . . . . . . . 8 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (𝑥 = 𝑢𝑦 = 𝑣))
31, 2e1a 40838 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
4 simpr 485 . . . . . . . . 9 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (𝜑𝜓))
51, 4e1a 40838 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   (𝜑𝜓)   )
6 simpl 483 . . . . . . . 8 ((𝜑𝜓) → 𝜑)
75, 6e1a 40838 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   𝜑   )
8 pm3.2 470 . . . . . . 7 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
93, 7, 8e11 40899 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
109in1 40782 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
1110eximi 1826 . . . 4 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
1211eximi 1826 . . 3 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
13 simpr 485 . . . . . . . 8 ((𝜑𝜓) → 𝜓)
145, 13e1a 40838 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   𝜓   )
15 pm3.2 470 . . . . . . 7 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜓 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
163, 14, 15e11 40899 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
1716in1 40782 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
1817eximi 1826 . . . 4 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
1918eximi 1826 . . 3 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
2012, 19jca 512 . 2 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
21 2uasbanhVD.1 . . 3 (𝜒 ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
2221biimpi 217 . . . . . . . . 9 (𝜒 → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
2322dfvd1ir 40784 . . . . . . . 8 (   𝜒   ▶   (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
24 simpl 483 . . . . . . . 8 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
2523, 24e1a 40838 . . . . . . 7 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
26 simpl 483 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
27262eximi 1827 . . . . . . . . . 10 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2825, 27e1a 40838 . . . . . . . . 9 (   𝜒   ▶   𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)   )
29 ax6e2ndeq 40770 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3029biimpri 229 . . . . . . . . 9 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))
3128, 30e1a 40838 . . . . . . . 8 (   𝜒   ▶   (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)   )
32 2sb5nd 40771 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
3331, 32e1a 40838 . . . . . . 7 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))   )
34 biimpr 221 . . . . . . . 8 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3534com12 32 . . . . . . 7 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3625, 33, 35e11 40899 . . . . . 6 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
37 simpr 485 . . . . . . . 8 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
3823, 37e1a 40838 . . . . . . 7 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
39 2sb5nd 40771 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
4031, 39e1a 40838 . . . . . . 7 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
41 biimpr 221 . . . . . . . 8 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4241com12 32 . . . . . . 7 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4338, 40, 42e11 40899 . . . . . 6 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜓   )
44 sban 2077 . . . . . . . 8 ([𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
4544sbbii 2072 . . . . . . 7 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
46 sban 2077 . . . . . . 7 ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4745, 46bitri 276 . . . . . 6 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
48 simplbi2comt 502 . . . . . . 7 (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓))))
4948com13 88 . . . . . 6 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 → (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) → [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓))))
5036, 43, 47, 49e110 40887 . . . . 5 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓)   )
51 2sb5nd 40771 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5231, 51e1a 40838 . . . . 5 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))   )
53 biimp 216 . . . . . 6 (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))) → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5453com12 32 . . . . 5 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) → (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5550, 52, 54e11 40899 . . . 4 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
5655in1 40782 . . 3 (𝜒 → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))
5721, 56sylbir 236 . 2 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))
5820, 57impbii 210 1 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wo 841  wal 1526   = wceq 1528  wex 1771  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ne 3014  df-v 3494  df-vd1 40781
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator