Metamath Proof Explorer


Theorem bj-2exbi

Description: Closed form of 2exbii . (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion bj-2exbi x y φ ψ x y φ x y ψ

Proof

Step Hyp Ref Expression
1 exbi y φ ψ y φ y ψ
2 1 alexbii x y φ ψ x y φ x y ψ