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 | |- ( ( 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 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-imim21 | |- ( ( 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 ) ) ) ) |