Theorem stdpc5v 1867

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

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem stdpc5v

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

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1737  ax-5 1839

This theorem is referenced by:  19.21v  1868  bj-ssb1a  32632  axc11next  38607