Theorem bj-axtd

Description: This implication, proved from propositional calculus only (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme |- ( A. x ph -> ph ) (modal T) implies the axiom scheme |- ( A. x ph -> E. x ph ) (modal D). See also bj-axdd2 and bj-axd2d . (Contributed by BJ, 16-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-axtd	⊢ ( ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) → ( ( ∀ 𝑥 𝜑 → 𝜑 ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		con2	⊢ ( ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) → ( 𝜑 → ¬ ∀ 𝑥 ¬ 𝜑 ) )
2		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
3	1 2	syl6ibr	⊢ ( ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) → ( 𝜑 → ∃ 𝑥 𝜑 ) )
4	3	imim2d	⊢ ( ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) → ( ( ∀ 𝑥 𝜑 → 𝜑 ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜑 ) ) )