Metamath Proof Explorer

Theorem axc5c4c711toc5

Description: Rederivation of sp from axc5c4c711 . Note that ax6 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011) Revised to use ax6v instead of ax6 , so that this rederivation requires only ax6v and propositional calculus. (Revised by BJ, 14-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax6v 
 |-  -. A. x -. x = y
2 pm2.21 
 |-  ( -. ph -> ( ph -> A. x ( A. x ph -> -. x = y ) ) )
3 ax-1 
 |-  ( ( ph -> A. x ( A. x ph -> -. x = y ) ) -> ( A. x A. x -. A. x A. x ( A. x ph -> -. x = y ) -> ( ph -> A. x ( A. x ph -> -. x = y ) ) ) )
4 axc5c4c711 
 |-  ( ( A. x A. x -. A. x A. x ( A. x ph -> -. x = y ) -> ( ph -> A. x ( A. x ph -> -. x = y ) ) ) -> ( A. x ph -> A. x -. x = y ) )
5 2 3 4 3syl 
 |-  ( -. ph -> ( A. x ph -> A. x -. x = y ) )
6 1 5 mtoi 
 |-  ( -. ph -> -. A. x ph )
7 6 con4i 
 |-  ( A. x ph -> ph )