Theorem hbimpgVD 45726

Description: Virtual deduction proof of hbimpg 45377. 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 45377 is hbimpgVD 45726 without virtual deductions and was automatically derived from hbimpgVD 45726. (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 2326	. . . 4 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥(𝜑 → ∀𝑥𝜑))
2		hba1 2326	. . . 4 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ∀𝑥∀𝑥(𝜓 → ∀𝑥𝜓))
3	1, 2	hban 2333	. . 3 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)))
4		idn2 45436	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶    ¬ 𝜑   )
5		idn1 45397	. . . . . . . . . . 11 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   )
6		simpl 488	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜑 → ∀𝑥𝜑))
7	5, 6	e1a 45450	. . . . . . . . . 10 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
8		hbntal 45376	. . . . . . . . . 10 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
9	7, 8	e1a 45450	. . . . . . . . 9 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
10		sp 2219	. . . . . . . . 9 ⊢ (∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
11	9, 10	e1a 45450	. . . . . . . 8 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
12		pm2.27 43	. . . . . . . 8 ⊢ (¬ 𝜑 → ((¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥 ¬ 𝜑))
13	4, 11, 12	e21 45552	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥 ¬ 𝜑   )
14		pm2.21 124	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
15	14	alimi 1844	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))
16	13, 15	e2 45454	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ,    ¬ 𝜑   ▶   ∀𝑥(𝜑 → 𝜓)   )
17	16	in2 45428	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (¬ 𝜑 → ∀𝑥(𝜑 → 𝜓))   )
18		simpr 490	. . . . . . . 8 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥(𝜓 → ∀𝑥𝜓))
19	5, 18	e1a 45450	. . . . . . 7 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥(𝜓 → ∀𝑥𝜓)   )
20		sp 2219	. . . . . . 7 ⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (𝜓 → ∀𝑥𝜓))
21	19, 20	e1a 45450	. . . . . 6 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥𝜓)   )
22		ax-1 6	. . . . . . 7 ⊢ (𝜓 → (𝜑 → 𝜓))
23	22	alimi 1844	. . . . . 6 ⊢ (∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓))
24		imim1 84	. . . . . 6 ⊢ ((𝜓 → ∀𝑥𝜓) → ((∀𝑥𝜓 → ∀𝑥(𝜑 → 𝜓)) → (𝜓 → ∀𝑥(𝜑 → 𝜓))))
25	21, 23, 24	e10 45517	. . . . 5 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   (𝜓 → ∀𝑥(𝜑 → 𝜓))   )
26		jao 975	. . . . 5 ⊢ ((¬ 𝜑 → ∀𝑥(𝜑 → 𝜓)) → ((𝜓 → ∀𝑥(𝜑 → 𝜓)) → ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
27	17, 25, 26	e11 45511	. . . 4 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
28		imor 867	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
29		imbi1 350	. . . . 5 ⊢ (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → (((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) ↔ ((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓))))
30	29	biimprcd 253	. . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) → ∀𝑥(𝜑 → 𝜓)) → (((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) → ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))))
31	27, 28, 30	e10 45517	. . 3 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
32	3, 31	gen11nv 45440	. 2 ⊢ (   (∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓))   ▶   ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))   )
33	32	in1 45394	1 ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-vd1 45393  df-vd2 45401

This theorem is used by: (None)