Metamath Proof Explorer

Theorem bibi12i

Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993)

Ref Expression
Hypotheses bibi2i.1 φ ψ
bibi12i.2 χ θ
Assertion bibi12i φ χ ψ θ


Step Hyp Ref Expression
1 bibi2i.1 φ ψ
2 bibi12i.2 χ θ
3 2 bibi2i φ χ φ θ
4 1 bibi1i φ θ ψ θ
5 3 4 bitri φ χ ψ θ