Metamath Proof Explorer


Theorem stdpc5v

Description: Version of stdpc5 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020) Revised to shorten 19.21v . (Revised by Wolf Lammen, 12-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 ax-5
 |-  ( ph -> A. x ph )
2 alim
 |-  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
3 1 2 syl5
 |-  ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )