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

Theorem hbimpgVD 39724
Description: Virtual deduction proof of hbimpg 39364. 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. hbimpg 39364 is hbimpgVD 39724 without virtual deductions and was automatically derived from hbimpgVD 39724. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 𝑥𝜓))   )
2:1: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
3:: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)), ¬ 𝜑   ▶   ¬ 𝜑   )
4:2: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥𝜑 → ∀𝑥¬ 𝜑)   )
5:4: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥¬ 𝜑)   )
6:3,5: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)), ¬ 𝜑   ▶   𝑥¬ 𝜑   )
7:: 𝜑 → (𝜑𝜓))
8:7: (∀𝑥¬ 𝜑 → ∀𝑥(𝜑𝜓))
9:6,8: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)), ¬ 𝜑   ▶   𝑥(𝜑𝜓)   )
10:9: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥(𝜑𝜓))   )
11:: (𝜓 → (𝜑𝜓))
12:11: (∀𝑥𝜓 → ∀𝑥(𝜑𝜓))
13:1: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜓 → ∀𝑥𝜓)   )
14:13: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
15:14,12: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑𝜓))   )
16:10,15: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
17:: ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
18:16,17: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
19:: (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥( 𝜑 → ∀𝑥𝜑))
20:: (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥𝑥( 𝜓 → ∀𝑥𝜓))
21:19,20: ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 𝑥𝜓)))
22:21,18: (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
qed:22: ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
Assertion
Ref Expression
hbimpgVD ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))

Proof of Theorem hbimpgVD
StepHypRef Expression
1 hba1 2325 . . . 4 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥(𝜑 → ∀𝑥𝜑))
2 hba1 2325 . . . 4 (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥𝑥(𝜓 → ∀𝑥𝜓))
31, 2hban 2305 . . 3 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4 idn2 39432 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5 idn1 39384 . . . . . . . . . . 11 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6 simpl 474 . . . . . . . . . . 11 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
75, 6e1a 39446 . . . . . . . . . 10 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
8 hbntal 39363 . . . . . . . . . 10 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
97, 8e1a 39446 . . . . . . . . 9 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
10 sp 2215 . . . . . . . . 9 (∀𝑥𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
119, 10e1a 39446 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥 ¬ 𝜑)   )
12 pm2.27 42 . . . . . . . 8 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
134, 11, 12e21 39550 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥 ¬ 𝜑   )
14 pm2.21 121 . . . . . . . 8 𝜑 → (𝜑𝜓))
1514alimi 1906 . . . . . . 7 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝜓))
1613, 15e2 39450 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥(𝜑𝜓)   )
1716in2 39424 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥(𝜑𝜓))   )
18 simpr 477 . . . . . . . 8 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
195, 18e1a 39446 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜓 → ∀𝑥𝜓)   )
20 sp 2215 . . . . . . 7 (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
2119, 20e1a 39446 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22 ax-1 6 . . . . . . 7 (𝜓 → (𝜑𝜓))
2322alimi 1906 . . . . . 6 (∀𝑥𝜓 → ∀𝑥(𝜑𝜓))
24 imim1 83 . . . . . 6 ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑𝜓)) → (𝜓 → ∀𝑥(𝜑𝜓))))
2521, 23, 24e10 39513 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑𝜓))   )
26 jao 983 . . . . 5 ((¬ 𝜑 → ∀𝑥(𝜑𝜓)) → ((𝜓 → ∀𝑥(𝜑𝜓)) → ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
2717, 25, 26e11 39507 . . . 4 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
28 imor 879 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
29 imbi1 338 . . . . 5 (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → (((𝜑𝜓) → ∀𝑥(𝜑𝜓)) ↔ ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3029biimprcd 241 . . . 4 (((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓)) → (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3127, 28, 30e10 39513 . . 3 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
323, 31gen11nv 39436 . 2 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
3332in1 39381 1 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  wal 1650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-vd1 39380  df-vd2 39388
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator