Theorem axc5c711 35528

Description: Proof of a single axiom that can replace ax-c5 35493, ax-c7 35495, and ax-11 2093 in a subsystem that includes these axioms plus ax-c4 35494 and ax-gen 1758 (and propositional calculus). See axc5c711toc5 35529, axc5c711toc7 35530, and axc5c711to11 35531 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 35521. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
axc5c711	⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Proof of Theorem axc5c711

Step	Hyp	Ref	Expression
1		ax-c5 35493	. . 3 ⊢ (∀𝑦𝜑 → 𝜑)
2		ax10fromc7 35505	. . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑)
3		ax-c7 35495	. . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑)
4	3	con1i 147	. . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
5	4	alimi 1774	. . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
6		ax-11 2093	. . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
7	2, 5, 6	3syl 18	. . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
8	1, 7	nsyl4 158	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑)
9		ax-c5 35493	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
10	8, 9	ja 175	1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Syntax hints:  ¬ wn 3  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-11 2093  ax-c5 35493  ax-c4 35494  ax-c7 35495

This theorem is referenced by:  axc5c711toc5  35529  axc5c711toc7  35530  axc5c711to11  35531