Theorem bj-axc4 36538

Description: Over minimal calculus, the modal axiom (4) (hba1 2292) and the modal axiom (K) (ax-4 1808) together imply axc4 2320. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
bj-axc4	⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))))

Proof of Theorem bj-axc4

Step	Hyp	Ref	Expression
1		bj-imim21 36493	1 ⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))))

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by: (None)