Theorem mpbir

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992)

	Ref	Expression
Hypotheses	mpbir.min	⊢ 𝜓
	mpbir.maj	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	mpbir	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		mpbir.min	⊢ 𝜓
2		mpbir.maj	⊢ ( 𝜑 ↔ 𝜓 )
3	2	biimpri	⊢ ( 𝜓 → 𝜑 )
4	1 3	ax-mp	⊢ 𝜑