Theorem hbimpgVD 41244

Description: Virtual deduction proof of hbimpg 40894. 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 40894 is hbimpgVD 41244 without virtual deductions and was automatically derived from hbimpgVD 41244. (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 2300	. . . 4 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥(𝜑 → ∀𝑥𝜑))
2		hba1 2300	. . . 4 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥∀𝑥(𝜓 → ∀𝑥𝜓))
3	1, 2	hban 2307	. . 3 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4		idn2 40953	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5		idn1 40914	. . . . . . . . . . 11 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6		simpl 485	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
7	5, 6	e1a 40967	. . . . . . . . . 10 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
8		hbntal 40893	. . . . . . . . . 10 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
9	7, 8	e1a 40967	. . . . . . . . 9 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
10		sp 2181	. . . . . . . . 9 ⊢ (∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
11	9, 10	e1a 40967	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
12		pm2.27 42	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
13	4, 11, 12	e21 41070	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥 ¬ 𝜑   )
14		pm2.21 123	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
15	14	alimi 1811	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))
16	13, 15	e2 40971	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥(𝜑 → 𝜓)   )
17	16	in2 40945	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))   )
18		simpr 487	. . . . . . . 8 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
19	5, 18	e1a 40967	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
20		sp 2181	. . . . . . 7 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
21	19, 20	e1a 40967	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22		ax-1 6	. . . . . . 7 ⊢ (𝜓 → (𝜑 → 𝜓))
23	22	alimi 1811	. . . . . 6 ⊢ (∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓))
24		imim1 83	. . . . . 6 ⊢ ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓)) → (𝜓 → ∀𝑥(𝜑 → 𝜓))))
25	21, 23, 24	e10 41034	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑 → 𝜓))   )
26		jao 957	. . . . 5 ⊢ ((¬ 𝜑 → ∀𝑥(𝜑 → 𝜓)) → ((𝜓 → ∀𝑥(𝜑 → 𝜓)) → ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
27	17, 25, 26	e11 41028	. . . 4 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
28		imor 849	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
29		imbi1 350	. . . . 5 ⊢ (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → (((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) ↔ ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
30	29	biimprcd 252	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓)) → (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))))
31	27, 28, 30	e10 41034	. . 3 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
32	3, 31	gen11nv 40957	. 2 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
33	32	in1 40911	1 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843  ∀wal 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-10 2144  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-vd1 40910  df-vd2 40918

This theorem is referenced by: (None)