Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axc5c711toc5 Structured version   Visualization version   Unicode version
Theorem axc5c711toc5 34204
Description: Rederivation of ax-c5 34168 from axc5c711 34203. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
axc5c711toc5 |- ( A. x ph -> ph )
Proof of Theorem axc5c711toc5
StepHypRef Expression
1 ax-1 6 . 2 |- ( A. x ph -> ( A. x A. x -. A. x A. x ph -> A. x ph ) )
2 axc5c711 34203 . 2 |- ( ( A. x A. x -. A. x A. x ph -> A. x ph ) -> ph )
31, 2syl 17 1 |- ( A. x ph -> ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> 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-11 2034  ax-c5 34168  ax-c4 34169  ax-c7 34170
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator