Theorem axc5c711 39037

Description: Proof of a single axiom that can replace ax-c5 39002, ax-c7 39004, and ax-11 2162 in a subsystem that includes these axioms plus ax-c4 39003 and ax-gen 1796 (and propositional calculus). See axc5c711toc5 39038, axc5c711toc7 39039, and axc5c711to11 39040 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 39030. (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 39002	. . 3 ⊢ (∀𝑦𝜑 → 𝜑)
2		ax10fromc7 39014	. . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑)
3		ax-c7 39004	. . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑)
4	3	con1i 147	. . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
5	4	alimi 1812	. . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑)
6		ax-11 2162	. . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
7	2, 5, 6	3syl 18	. . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑)
8	1, 7	nsyl4 158	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑)
9		ax-c5 39002	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
10	8, 9	ja 186	1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Syntax hints:  ¬ wn 3  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-11 2162  ax-c5 39002  ax-c4 39003  ax-c7 39004

This theorem is referenced by:  axc5c711toc5  39038  axc5c711toc7  39039  axc5c711to11  39040