Theorem mpbi

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993)

	Ref	Expression
Hypotheses	mpbi.min	|- ph
	mpbi.maj	|- ( ph <-> ps )
Assertion	mpbi	|- ps

Proof

Step	Hyp	Ref	Expression
1		mpbi.min	|- ph
2		mpbi.maj	|- ( ph <-> ps )
3	2	biimpi	|- ( ph -> ps )
4	1 3	ax-mp	|- ps