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

Metamath Proof Explorer

Theorem 3anibar

Description: Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008)

		Ref	Expression
	Hypothesis	3anibar.1	$⊢ (φ \land ψ \land χ) \to (θ \leftrightarrow (χ \land τ))$
	Assertion	3anibar	$⊢ (φ \land ψ \land χ) \to (θ \leftrightarrow τ)$

Step	Hyp	Ref	Expression
1		3anibar.1	$⊢ (φ \land ψ \land χ) \to (θ \leftrightarrow (χ \land τ))$
2		simp3	$⊢ (φ \land ψ \land χ) \to χ$
3	2 1	mpbirand	$⊢ (φ \land ψ \land χ) \to (θ \leftrightarrow τ)$