Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-nmp Unicode version

Axiom ax-nmp 24979
Description: If  ph is a theorem then it holds in the next step. (Contributed by FL, 20-Mar-2011.)
Ref Expression
ax-nmp.1  |-  ph
Ref Expression
ax-nmp  |-  () ph

Detailed syntax breakdown of Axiom ax-nmp
StepHypRef Expression
1 wph . 2  wff  ph
21wcirc 24972 1  wff  () ph
Colors of variables: wff set class
This axiom is referenced by:  impxt  24983
  Copyright terms: Public domain W3C validator