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 in each step implies it is true in the previous step, and is eventually true, then is true in the first step. (Contributed by Mario Carneiro, 30-Aug-2016.)
Assertion
Ref Expression
ltl4ev

Proof of Theorem ltl4ev
StepHypRef Expression
1 df-dia 24392 . . 3
2 con34b 283 . . . . . . 7
3 ax-ltl2 24387 . . . . . . . 8
43imbi2i 303 . . . . . . 7
52, 4bitri 240 . . . . . 6
65bibox 24394 . . . . 5
7 ax-ltl4 24389 . . . . . 6
87ex 423 . . . . 5
96, 8sylbi 187 . . . 4
109con1d 116 . . 3
111, 10syl5bi 208 . 2
1211imp 418 1
 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