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

Axiom ax-ltl4 24977
Description: Suppose that it is always true that if  ph is true in the current step then  ph is true in the next step. Suppose that  ph is true in the first step. Then  ph is always true. (Contributed by FL, 20-Mar-2011.)
Assertion
Ref Expression
ax-ltl4  |-  ( ( [.] ( ph  ->  ()
ph )  /\  ph )  ->  [.] ph )

Detailed syntax breakdown of Axiom ax-ltl4
StepHypRef Expression
1 wph . . . . 5  wff  ph
21wcirc 24972 . . . . 5  wff  () ph
31, 2wi 4 . . . 4  wff  ( ph  ->  () ph )
43wbox 24970 . . 3  wff  [.] ( ph  ->  () ph )
54, 1wa 358 . 2  wff  ( [.] ( ph  ->  () ph )  /\  ph )
61wbox 24970 . 2  wff  [.] ph
75, 6wi 4 1  wff  ( ( [.] ( ph  ->  ()
ph )  /\  ph )  ->  [.] ph )
Colors of variables: wff set class
This axiom is referenced by:  ltl4ev  24992  alalifal  25003
  Copyright terms: Public domain W3C validator