Theorem bj-axc4

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

	Ref	Expression
Assertion	bj-axc4	$$⊢\left(\forall x\phi \to \forall x\forall x\phi \right)\to \left(\left(\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\forall x\phi \to \forall x\psi \right)\right)\to \left(\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-imim21	$$⊢\left(\forall x\phi \to \forall x\forall x\phi \right)\to \left(\left(\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\forall x\phi \to \forall x\psi \right)\right)\to \left(\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)\right)\right)$$