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

Metamath Proof Explorer

Theorem mpbii

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Oct-2012)

	Ref	Expression
Hypotheses	mpbii.min	$⊢ ψ$
	mpbii.maj	$⊢ φ \to (ψ \leftrightarrow χ)$
Assertion	mpbii	$⊢ φ \to χ$

Proof

Step	Hyp	Ref	Expression
1		mpbii.min	$⊢ ψ$
2		mpbii.maj	$⊢ φ \to (ψ \leftrightarrow χ)$
3	1	a1i	$⊢ φ \to ψ$
4	3 2	mpbid	$⊢ φ \to χ$