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 φ