Metamath Proof Explorer


Theorem bj-alexim

Description: Closed form of aleximi . Note: this proof is shorter, so aleximi could be deduced from it ( exim would have to be proved first, see bj-eximALT but its proof is shorter (currently almost a subproof of aleximi )). (Contributed by BJ, 8-Nov-2021)

Ref Expression
Assertion bj-alexim x φ ψ χ x φ x ψ x χ

Proof

Step Hyp Ref Expression
1 alim x φ ψ χ x φ x ψ χ
2 exim x ψ χ x ψ x χ
3 1 2 syl6 x φ ψ χ x φ x ψ x χ