Theorem axc5c711 38900

Description: Proof of a single axiom that can replace ax-c5 38865, ax-c7 38867, and ax-11 2155 in a subsystem that includes these axioms plus ax-c4 38866 and ax-gen 1792 (and propositional calculus). See axc5c711toc5 38901, axc5c711toc7 38902, and axc5c711to11 38903 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 38893. (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 38865	. . 3 ⊢ (∀𝑦𝜑 → 𝜑)
2		ax10fromc7 38877	. . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑)
3		ax-c7 38867	. . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑)
4	3	con1i 147	. . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
5	4	alimi 1808	. . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
6		ax-11 2155	. . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
7	2, 5, 6	3syl 18	. . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
8	1, 7	nsyl4 158	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑)
9		ax-c5 38865	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
10	8, 9	ja 186	1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Syntax hints:  ¬ wn 3  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-11 2155  ax-c5 38865  ax-c4 38866  ax-c7 38867

This theorem is referenced by:  axc5c711toc5  38901  axc5c711toc7  38902  axc5c711to11  38903