Metamath Proof Explorer

Theorem 2sp

Description: A double specialization (see sp ). Another double specialization, closer to PM*11.1, is 2stdpc4 . (Contributed by BJ, 15-Sep-2018)

Ref Expression
Assertion 2sp 
|- ( A. x A. y ph -> ph )

Proof

Step Hyp Ref Expression
1 sp 
 |-  ( A. y ph -> ph )
2 1 sps 
 |-  ( A. x A. y ph -> ph )