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 37958
Description: Virtual deduction proof of hbimpg 37587. 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 37587 is hbimpgVD 37958 without virtual deductions and was automatically derived from hbimpgVD 37958. (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 2136 . . . 4 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥(𝜑 → ∀𝑥𝜑))
2 hba1 2136 . . . 4 (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥𝑥(𝜓 → ∀𝑥𝜓))
31, 2hban 2112 . . 3 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4 idn2 37655 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5 idn1 37607 . . . . . . . . . . 11 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6 simpl 471 . . . . . . . . . . 11 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
75, 6e1a 37669 . . . . . . . . . 10 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
8 hbntal 37586 . . . . . . . . . 10 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
97, 8e1a 37669 . . . . . . . . 9 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
10 sp 2040 . . . . . . . . 9 (∀𝑥𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
119, 10e1a 37669 . . . . . . . 8 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥 ¬ 𝜑)   )
12 pm2.27 40 . . . . . . . 8 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
134, 11, 12e21 37774 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥 ¬ 𝜑   )
14 pm2.21 118 . . . . . . . 8 𝜑 → (𝜑𝜓))
1514alimi 1729 . . . . . . 7 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝜓))
1613, 15e2 37673 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   𝑥(𝜑𝜓)   )
1716in2 37647 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝜑 → ∀𝑥(𝜑𝜓))   )
18 simpr 475 . . . . . . . 8 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
195, 18e1a 37669 . . . . . . 7 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥(𝜓 → ∀𝑥𝜓)   )
20 sp 2040 . . . . . . 7 (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
2119, 20e1a 37669 . . . . . 6 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22 ax-1 6 . . . . . . 7 (𝜓 → (𝜑𝜓))
2322alimi 1729 . . . . . 6 (∀𝑥𝜓 → ∀𝑥(𝜑𝜓))
24 imim1 80 . . . . . 6 ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑𝜓)) → (𝜓 → ∀𝑥(𝜑𝜓))))
2521, 23, 24e10 37736 . . . . 5 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑𝜓))   )
26 jao 532 . . . . 5 ((¬ 𝜑 → ∀𝑥(𝜑𝜓)) → ((𝜓 → ∀𝑥(𝜑𝜓)) → ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
2717, 25, 26e11 37730 . . . 4 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
28 imor 426 . . . 4 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
29 imbi1 335 . . . . 5 (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → (((𝜑𝜓) → ∀𝑥(𝜑𝜓)) ↔ ((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3029biimprcd 238 . . . 4 (((¬ 𝜑𝜓) → ∀𝑥(𝜑𝜓)) → (((𝜑𝜓) ↔ (¬ 𝜑𝜓)) → ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
3127, 28, 30e10 37736 . . 3 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
323, 31gen11nv 37659 . 2 (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓))   )
3332in1 37604 1 ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-vd1 37603  df-vd2 37611
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator