Theorem hbimpgVD 42477

Description: Virtual deduction proof of hbimpg 42127. 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 42127 is hbimpgVD 42477 without virtual deductions and was automatically derived from hbimpgVD 42477. (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 2293	. . . 4 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥(𝜑 → ∀𝑥𝜑))
2		hba1 2293	. . . 4 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥∀𝑥(𝜓 → ∀𝑥𝜓))
3	1, 2	hban 2300	. . 3 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4		idn2 42186	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5		idn1 42147	. . . . . . . . . . 11 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6		simpl 482	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
7	5, 6	e1a 42200	. . . . . . . . . 10 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
8		hbntal 42126	. . . . . . . . . 10 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
9	7, 8	e1a 42200	. . . . . . . . 9 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
10		sp 2179	. . . . . . . . 9 ⊢ (∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
11	9, 10	e1a 42200	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
12		pm2.27 42	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
13	4, 11, 12	e21 42303	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥 ¬ 𝜑   )
14		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
15	14	alimi 1817	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))
16	13, 15	e2 42204	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥(𝜑 → 𝜓)   )
17	16	in2 42178	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))   )
18		simpr 484	. . . . . . . 8 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
19	5, 18	e1a 42200	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
20		sp 2179	. . . . . . 7 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
21	19, 20	e1a 42200	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22		ax-1 6	. . . . . . 7 ⊢ (𝜓 → (𝜑 → 𝜓))
23	22	alimi 1817	. . . . . 6 ⊢ (∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓))
24		imim1 83	. . . . . 6 ⊢ ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓)) → (𝜓 → ∀𝑥(𝜑 → 𝜓))))
25	21, 23, 24	e10 42267	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑 → 𝜓))   )
26		jao 957	. . . . 5 ⊢ ((¬ 𝜑 → ∀𝑥(𝜑 → 𝜓)) → ((𝜓 → ∀𝑥(𝜑 → 𝜓)) → ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
27	17, 25, 26	e11 42261	. . . 4 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
28		imor 849	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
29		imbi1 347	. . . . 5 ⊢ (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → (((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) ↔ ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
30	29	biimprcd 249	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓)) → (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))))
31	27, 28, 30	e10 42267	. . 3 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
32	3, 31	gen11nv 42190	. 2 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
33	32	in1 42144	1 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-10 2140  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-vd1 42143  df-vd2 42151

This theorem is referenced by: (None)