This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axc5c711to11

Description: Rederivation of ax-11 from axc5c711 . Note that ax-c7 and ax-11 are not used by the rederivation. The use of alimi (which uses ax-c5 ) is allowed since we have already proved axc5c711toc5 . (Contributed by NM, 19-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axc5c711toc7 
 |-  ( -. A. y -. A. y -. A. x A. y ph -> -. A. x A. y ph )
2 1 con4i 
 |-  ( A. x A. y ph -> A. y -. A. y -. A. x A. y ph )
3 pm2.21 
 |-  ( -. A. x A. y -. A. x A. y ph -> ( A. x A. y -. A. x A. y ph -> A. x ph ) )
4 axc5c711 
 |-  ( ( A. x A. y -. A. x A. y ph -> A. x ph ) -> ph )
5 3 4 syl 
 |-  ( -. A. x A. y -. A. x A. y ph -> ph )
6 5 alimi 
 |-  ( A. x -. A. x A. y -. A. x A. y ph -> A. x ph )
7 axc5c711toc7 
 |-  ( -. A. x -. A. x A. y -. A. x A. y ph -> A. y -. A. x A. y ph )
8 6 7 nsyl4 
 |-  ( -. A. y -. A. x A. y ph -> A. x ph )
9 8 alimi 
 |-  ( A. y -. A. y -. A. x A. y ph -> A. y A. x ph )
10 2 9 syl 
 |-  ( A. x A. y ph -> A. y A. x ph )