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

Theorem ltl4ev 24404
Description: The contrapositive of ax-ltl4 24389. If the truth of  ph in each step implies it is true in the previous step, and  ph is eventually true, then  ph is true in the first step. (Contributed by Mario Carneiro, 30-Aug-2016.)
Assertion
Ref Expression
ltl4ev  |-  ( ( [.] ( () ph  ->  ph )  /\  <> ph )  ->  ph )

Proof of Theorem ltl4ev
StepHypRef Expression
1 df-dia 24392 . . 3  |-  ( <> ph  <->  -. 
[.]  -.  ph )
2 con34b 283 . . . . . . 7  |-  ( ( () ph  ->  ph )  <->  ( -.  ph  ->  -.  () ph ) )
3 ax-ltl2 24387 . . . . . . . 8  |-  ( -.  () ph  <->  ()  -.  ph )
43imbi2i 303 . . . . . . 7  |-  ( ( -.  ph  ->  -.  () ph )  <->  ( -.  ph  ->  ()  -.  ph )
)
52, 4bitri 240 . . . . . 6  |-  ( ( () ph  ->  ph )  <->  ( -.  ph  ->  ()  -.  ph ) )
65bibox 24394 . . . . 5  |-  ( [.] ( () ph  ->  ph )  <->  [.] ( -.  ph  ->  ()  -.  ph )
)
7 ax-ltl4 24389 . . . . . 6  |-  ( ( [.] ( -.  ph  ->  ()  -.  ph )  /\  -.  ph )  ->  [.]  -.  ph )
87ex 423 . . . . 5  |-  ( [.] ( -.  ph  ->  () 
-.  ph )  ->  ( -.  ph  ->  [.]  -.  ph ) )
96, 8sylbi 187 . . . 4  |-  ( [.] ( () ph  ->  ph )  ->  ( -.  ph 
->  [.]  -.  ph )
)
109con1d 116 . . 3  |-  ( [.] ( () ph  ->  ph )  ->  ( -.  [.]  -.  ph  ->  ph )
)
111, 10syl5bi 208 . 2  |-  ( [.] ( () ph  ->  ph )  ->  ( <> ph  ->  ph ) )
1211imp 418 1  |-  ( ( [.] ( () ph  ->  ph )  /\  <> ph )  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   [.]wbox 24382   <>wdia 24383   ()wcirc 24384
This theorem is referenced by:  evpexun  24410  untind  24430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ltl1 24386  ax-ltl2 24387  ax-ltl4 24389  ax-lmp 24390
This theorem depends on definitions:  df-bi 177  df-an 360  df-dia 24392
  Copyright terms: Public domain W3C validator