Metamath Proof Explorer

Theorem exbiri

Description: Inference form of exbir . This proof is exbiriVD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof shortened by Wolf Lammen, 27-Jan-2013)

Ref Expression
Hypothesis exbiri.1 φ ψ χ θ
Assertion exbiri φ ψ θ χ


Step Hyp Ref Expression
1 exbiri.1 φ ψ χ θ
2 1 biimpar φ ψ θ χ
3 2 exp31 φ ψ θ χ