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 ( ( 𝜑𝜓 ) → 𝜓 )
Assertion bj-looinvi ( ( 𝜓𝜑 ) → 𝜑 )

Proof

Step Hyp Ref Expression
1 bj-looinvi.1 ( ( 𝜑𝜓 ) → 𝜓 )
2 looinv ( ( ( 𝜑𝜓 ) → 𝜓 ) → ( ( 𝜓𝜑 ) → 𝜑 ) )
3 1 2 ax-mp ( ( 𝜓𝜑 ) → 𝜑 )