Theorem hbimpgVD 44944

Description: Virtual deduction proof of hbimpg 44595. 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 44595 is hbimpgVD 44944 without virtual deductions and was automatically derived from hbimpgVD 44944. (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

Step	Hyp	Ref	Expression
1		hba1 2295	. . . 4 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥(𝜑 → ∀𝑥𝜑))
2		hba1 2295	. . . 4 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥∀𝑥(𝜓 → ∀𝑥𝜓))
3	1, 2	hban 2302	. . 3 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4		idn2 44654	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5		idn1 44615	. . . . . . . . . . 11 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6		simpl 482	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
7	5, 6	e1a 44668	. . . . . . . . . 10 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
8		hbntal 44594	. . . . . . . . . 10 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
9	7, 8	e1a 44668	. . . . . . . . 9 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
10		sp 2186	. . . . . . . . 9 ⊢ (∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
11	9, 10	e1a 44668	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
12		pm2.27 42	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
13	4, 11, 12	e21 44770	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥 ¬ 𝜑   )
14		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
15	14	alimi 1812	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))
16	13, 15	e2 44672	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥(𝜑 → 𝜓)   )
17	16	in2 44646	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))   )
18		simpr 484	. . . . . . . 8 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
19	5, 18	e1a 44668	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
20		sp 2186	. . . . . . 7 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
21	19, 20	e1a 44668	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22		ax-1 6	. . . . . . 7 ⊢ (𝜓 → (𝜑 → 𝜓))
23	22	alimi 1812	. . . . . 6 ⊢ (∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓))
24		imim1 83	. . . . . 6 ⊢ ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓)) → (𝜓 → ∀𝑥(𝜑 → 𝜓))))
25	21, 23, 24	e10 44735	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑 → 𝜓))   )
26		jao 962	. . . . 5 ⊢ ((¬ 𝜑 → ∀𝑥(𝜑 → 𝜓)) → ((𝜓 → ∀𝑥(𝜑 → 𝜓)) → ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
27	17, 25, 26	e11 44729	. . . 4 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
28		imor 853	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
29		imbi1 347	. . . . 5 ⊢ (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → (((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) ↔ ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
30	29	biimprcd 250	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓)) → (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))))
31	27, 28, 30	e10 44735	. . 3 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
32	3, 31	gen11nv 44658	. 2 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
33	32	in1 44612	1 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-vd1 44611  df-vd2 44619

This theorem is referenced by: (None)