Metamath Proof Explorer


Theorem ral2imi

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006) Allow shortening of ralim . (Revised by Wolf Lammen, 1-Dec-2019)

Ref Expression
Hypothesis ral2imi.1 φψχ
Assertion ral2imi xAφxAψxAχ

Proof

Step Hyp Ref Expression
1 ral2imi.1 φψχ
2 df-ral xAφxxAφ
3 1 imim3i xAφxAψxAχ
4 3 al2imi xxAφxxAψxxAχ
5 df-ral xAψxxAψ
6 df-ral xAχxxAχ
7 4 5 6 3imtr4g xxAφxAψxAχ
8 2 7 sylbi xAφxAψxAχ