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

Axiom ax-lmp 24978
Description: If  ph is a theorem then it always holds. (Contributed by FL, 22-Feb-2011.)
Hypothesis
Ref Expression
ax-lmp.1  |-  ph
Assertion
Ref Expression
ax-lmp  |-  [.] ph

Detailed syntax breakdown of Axiom ax-lmp
StepHypRef Expression
1 wph . 2  wff  ph
21wbox 24970 1  wff  [.] ph
Colors of variables: wff set class
This axiom is referenced by:  impbox  24981  evpexun  24998  trtrst  25016  untindd  25019  axlmp2  25025  axlmp3  25026
  Copyright terms: Public domain W3C validator