Theorem axc11-o 34236

Description: Show that ax-c11 34172 can be derived from ax-c11n 34173 and ax-12 2047. An open problem is whether this theorem can be derived from ax-c11n 34173 and the others when ax-12 2047 is replaced with ax-c15 34174 or ax12v 2048. See theorem axc11nfromc11 34211 for the rederivation of ax-c11n 34173 from axc11 2314.

Normally, axc11 2314 should be used rather than ax-c11 34172 or axc11-o 34236, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
axc11-o	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )

Proof of Theorem axc11-o

Step	Hyp	Ref	Expression
1		ax-c11n 34173	. 2 |- ( A. x x = y -> A. y y = x )
2		ax12 2304	. . . 4 |- ( y = x -> ( A. x ph -> A. y ( y = x -> ph ) ) )
3	2	equcoms 1947	. . 3 |- ( x = y -> ( A. x ph -> A. y ( y = x -> ph ) ) )
4	3	sps-o 34193	. 2 |- ( A. x x = y -> ( A. x ph -> A. y ( y = x -> ph ) ) )
5		pm2.27 42	. . 3 |- ( y = x -> ( ( y = x -> ph ) -> ph ) )
6	5	al2imi 1743	. 2 |- ( A. y y = x -> ( A. y ( y = x -> ph ) -> A. y ph ) )
7	1, 4, 6	sylsyld 61	1 |- ( A. x x = y -> ( A. x ph -> A. y ph ) )

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246  ax-c5 34168  ax-c11n 34173

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)