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 39657
Description: Virtual deduction proof of hbimpg 39290. 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 39290 is hbimpgVD 39657 without virtual deductions and was automatically derived from hbimpgVD 39657. (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 2298 . . . 4 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥(𝜑 → ∀𝑥𝜑))
2 hba1 2298 . . . 4 (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥𝑥(𝜓 → ∀𝑥𝜓))
31, 2hban 2275 . . 3 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4 idn2 39358 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5 idn1 39310 . . . . . . . . . . 11 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6 simpl 474 . . . . . . . . . . 11 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
75, 6e1a 39372 . . . . . . . . . 10 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
8 hbntal 39289 . . . . . . . . . 10 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
97, 8e1a 39372 . . . . . . . . 9 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
10 sp 2200 . . . . . . . . 9 (∀𝑥𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
119, 10e1a 39372 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥 ¬ 𝜑)   )
12 pm2.27 42 . . . . . . . 8 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
134, 11, 12e21 39477 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥 ¬ 𝜑   )
14 pm2.21 120 . . . . . . . 8 𝜑 → (𝜑𝜓))
1514alimi 1888 . . . . . . 7 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝜓))
1613, 15e2 39376 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥(𝜑𝜓)   )
1716in2 39350 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥(𝜑𝜓))   )
18 simpr 479 . . . . . . . 8 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
195, 18e1a 39372 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜓 → ∀𝑥𝜓)   )
20 sp 2200 . . . . . . 7 (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
2119, 20e1a 39372 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22 ax-1 6 . . . . . . 7 (𝜓 → (𝜑𝜓))
2322alimi 1888 . . . . . 6 (∀𝑥𝜓 → ∀𝑥(𝜑𝜓))
24 imim1 83 . . . . . 6 ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑𝜓)) → (𝜓 → ∀𝑥(𝜑𝜓))))
2521, 23, 24e10 39439 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑𝜓))   )
26 jao 535 . . . . 5 ((¬ 𝜑 → ∀𝑥(𝜑𝜓)) → ((𝜓 → ∀𝑥(𝜑𝜓)) → ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
2717, 25, 26e11 39433 . . . 4 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
28 imor 427 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
29 imbi1 336 . . . . 5 (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → (((𝜑𝜓) → ∀𝑥(𝜑𝜓)) ↔ ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3029biimprcd 240 . . . 4 (((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓)) → (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3127, 28, 30e10 39439 . . 3 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
323, 31gen11nv 39362 . 2 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
3332in1 39307 1 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wal 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-vd1 39306  df-vd2 39314
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator