Theorem ax172 16485

Description: Quantification of two variables over a formula in which they do not occur.

Assertion

Ref	Expression
ax172	|- (ph -> A.xA.yph)

Distinct variable group:   ph,x,y

Proof of Theorem ax172

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ph -> A.yph)
2		ax-17 1317	. 2 |- (A.yph -> A.xA.yph)
3	1, 2	syl 12	1 |- (ph -> A.xA.yph)

Syntax hints:   -> wi 3  A.wal 1296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-17 1317

Copyright terms: Public domain