Metamath Proof Explorer


Theorem bj-looinvii

Description: Inference associated with bj-looinvi . (Contributed by BJ, 30-Mar-2020)

Ref Expression
Hypotheses bj-looinvii.1
|- ( ( ph -> ps ) -> ps )
bj-looinvii.2
|- ( ps -> ph )
Assertion bj-looinvii
|- ph

Proof

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