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	$$⊢\left(\forall x\neg \phi \to \neg \phi \right)\to \left(\left(\forall x\phi \to \phi \right)\to \left(\forall x\phi \to \exists x\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		con2	$$⊢\left(\forall x\neg \phi \to \neg \phi \right)\to \left(\phi \to \neg \forall x\neg \phi \right)$$
2		df-ex	$$⊢\exists x\phi \leftrightarrow \neg \forall x\neg \phi$$
3	1 2	syl6ibr	$$⊢\left(\forall x\neg \phi \to \neg \phi \right)\to \left(\phi \to \exists x\phi \right)$$
4	3	imim2d	$$⊢\left(\forall x\neg \phi \to \neg \phi \right)\to \left(\left(\forall x\phi \to \phi \right)\to \left(\forall x\phi \to \exists x\phi \right)\right)$$