Metamath Proof Explorer


Theorem bj-looinvi

Description: Inference associated with looinv . Its associated inference is bj-looinvii . (Contributed by BJ, 30-Mar-2020)

Ref Expression
Hypothesis bj-looinvi.1
|- ( ( ph -> ps ) -> ps )
Assertion bj-looinvi
|- ( ( ps -> ph ) -> ph )

Proof

Step Hyp Ref Expression
1 bj-looinvi.1
 |-  ( ( ph -> ps ) -> ps )
2 looinv
 |-  ( ( ( ph -> ps ) -> ps ) -> ( ( ps -> ph ) -> ph ) )
3 1 2 ax-mp
 |-  ( ( ps -> ph ) -> ph )