Theorem bj-looinvii

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

	Ref	Expression
Hypotheses	bj-looinvii.1	$$⊢\left(\phi \to \psi \right)\to \psi$$
	bj-looinvii.2	$$⊢\psi \to \phi$$
Assertion	bj-looinvii	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		bj-looinvii.1	$$⊢\left(\phi \to \psi \right)\to \psi$$
2		bj-looinvii.2	$$⊢\psi \to \phi$$
3	1	bj-looinvi	$$⊢\left(\psi \to \phi \right)\to \phi$$
4	2 3	ax-mp	$$⊢\phi$$