Theorem bj-axc4 32581

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

Assertion

Ref	Expression
bj-axc4	|- ( ( A. x ph -> A. x A. x ph ) -> ( ( A. x ( A. x ph -> ps ) -> ( A. x A. x ph -> A. x ps ) ) -> ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) ) )

Proof of Theorem bj-axc4

Step	Hyp	Ref	Expression
1		bj-imim21 32539	1 |- ( ( A. x ph -> A. x A. x ph ) -> ( ( A. x ( A. x ph -> ps ) -> ( A. x A. x ph -> A. x ps ) ) -> ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) ) )

Syntax hints:   -> wi 4   A.wal 1481

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

This theorem is referenced by: (None)