Metamath Proof Explorer

Theorem bi1imp

Description: Importation inference similar to imp , except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017)

Ref Expression
Hypothesis bi1imp.1 φ ψ χ
Assertion bi1imp φ ψ χ


Step Hyp Ref Expression
1 bi1imp.1 φ ψ χ
2 1 biimpi φ ψ χ
3 2 imp φ ψ χ