Metamath Proof Explorer


Theorem 3anibar

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

Ref Expression
Hypothesis 3anibar.1 φ ψ χ θ χ τ
Assertion 3anibar φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 3anibar.1 φ ψ χ θ χ τ
2 simp3 φ ψ χ χ
3 2 1 mpbirand φ ψ χ θ τ