This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem biimpi

Description: Infer an implication from a logical equivalence. Inference associated with biimp . (Contributed by NM, 29-Dec-1992)

		Ref	Expression
	Hypothesis	biimpi.1	$⊢ φ \leftrightarrow ψ$
	Assertion	biimpi	$⊢ φ \to ψ$

Step	Hyp	Ref	Expression
1		biimpi.1	$⊢ φ \leftrightarrow ψ$
2		biimp	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$
3	1 2	ax-mp	$⊢ φ \to ψ$