Theorem axc5c711 36618

Description: Proof of a single axiom that can replace ax-c5 36583, ax-c7 36585, and ax-11 2160 in a subsystem that includes these axioms plus ax-c4 36584 and ax-gen 1803 (and propositional calculus). See axc5c711toc5 36619, axc5c711toc7 36620, and axc5c711to11 36621 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 36611. (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 36583	. . 3 ⊢ (∀𝑦𝜑 → 𝜑)
2		ax10fromc7 36595	. . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑)
3		ax-c7 36585	. . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑)
4	3	con1i 149	. . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
5	4	alimi 1819	. . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
6		ax-11 2160	. . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
7	2, 5, 6	3syl 18	. . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
8	1, 7	nsyl4 161	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑)
9		ax-c5 36583	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
10	8, 9	ja 189	1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Syntax hints:  ¬ wn 3  ∀wal 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-11 2160  ax-c5 36583  ax-c4 36584  ax-c7 36585

This theorem is referenced by:  axc5c711toc5  36619  axc5c711toc7  36620  axc5c711to11  36621