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

Metamath Proof Explorer

Theorem mpgbir

Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994) (Proof shortened by Stefan Allan, 28-Oct-2008)

	Ref	Expression
Hypotheses	mpgbir.1	$⊢ φ \leftrightarrow \forall x ψ$
	mpgbir.2	$⊢ ψ$
Assertion	mpgbir	$⊢ φ$

Proof

Step	Hyp	Ref	Expression
1		mpgbir.1	$⊢ φ \leftrightarrow \forall x ψ$
2		mpgbir.2	$⊢ ψ$
3	2	ax-gen	$⊢ \forall x ψ$
4	3 1	mpbir	$⊢ φ$