Metamath Proof Explorer

Theorem bi2imp

Description: Importation inference similar to imp , except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017)

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


Step Hyp Ref Expression
1 bi2imp.1 φ ψ χ
2 1 biimpi φ ψ χ
3 2 biimpa φ ψ χ