Metamath Proof Explorer


Theorem bj-looinvii

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

Ref Expression
Hypotheses bj-looinvii.1 ( ( 𝜑𝜓 ) → 𝜓 )
bj-looinvii.2 ( 𝜓𝜑 )
Assertion bj-looinvii 𝜑

Proof

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