Metamath Proof Explorer

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 
|- ( ( A. x -. ph -> -. ph ) -> ( ( A. x ph -> ph ) -> ( A. x ph -> E. x ph ) ) )

Proof

Step Hyp Ref Expression
1 con2 
 |-  ( ( A. x -. ph -> -. ph ) -> ( ph -> -. A. x -. ph ) )
2 df-ex 
 |-  ( E. x ph <-> -. A. x -. ph )
3 1 2 syl6ibr 
 |-  ( ( A. x -. ph -> -. ph ) -> ( ph -> E. x ph ) )
4 3 imim2d 
 |-  ( ( A. x -. ph -> -. ph ) -> ( ( A. x ph -> ph ) -> ( A. x ph -> E. x ph ) ) )