Metamath Proof Explorer

Theorem al2im

Description: Closed form of al2imi . Version of alim for a nested implication. (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Assertion al2im 
|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )

Proof

Step Hyp Ref Expression
1 alim 
 |-  ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> A. x ( ps -> ch ) ) )
2 alim 
 |-  ( A. x ( ps -> ch ) -> ( A. x ps -> A. x ch ) )
3 1 2 syl6 
 |-  ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )