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

Theorem ltl4ev 25095
Description: The contrapositive of ax-ltl4 25080. 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 25083 . . 3  |-  ( <> ph  <->  -. 
[.]  -.  ph )
2 con34b 283 . . . . . . 7  |-  ( ( () ph  ->  ph )  <->  ( -.  ph  ->  -.  () ph ) )
3 ax-ltl2 25078 . . . . . . . 8  |-  ( -.  () ph  <->  ()  -.  ph )
43imbi2i 303 . . . . . . 7  |-  ( ( -.  ph  ->  -.  () ph )  <->  ( -.  ph  ->  ()  -.  ph )
)
52, 4bitri 240 . . . . . 6  |-  ( ( () ph  ->  ph )  <->  ( -.  ph  ->  ()  -.  ph ) )
65bibox 25085 . . . . 5  |-  ( [.] ( () ph  ->  ph )  <->  [.] ( -.  ph  ->  ()  -.  ph )
)
7 ax-ltl4 25080 . . . . . 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 25073   <>wdia 25074   ()wcirc 25075
This theorem is referenced by:  evpexun  25101  untind  25121
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ltl1 25077  ax-ltl2 25078  ax-ltl4 25080  ax-lmp 25081
This theorem depends on definitions:  df-bi 177  df-an 360  df-dia 25083
  Copyright terms: Public domain W3C validator