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 φ