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

Theorem nxtor 25088
Description:  (
ph  \/  ps ) holds in the next step iff  ph holds in the next step or  ps holds in the next step. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
nxtor  |-  ( () ( ph  \/  ps ) 
<->  ( () ph  \/  () ps ) )

Proof of Theorem nxtor
StepHypRef Expression
1 ax-ltl2 25078 . . . 4  |-  ( -.  () ph  <->  ()  -.  ph )
2 df-or 359 . . . . . 6  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
32binxt 25087 . . . . 5  |-  ( () ( ph  \/  ps ) 
<->  () ( -.  ph  ->  ps ) )
4 ax-ltl3 25079 . . . . 5  |-  ( () ( -.  ph  ->  ps )  ->  ( ()  -.  ph  ->  () ps ) )
53, 4sylbi 187 . . . 4  |-  ( () ( ph  \/  ps )  ->  ( ()  -.  ph 
->  () ps ) )
61, 5syl5bi 208 . . 3  |-  ( () ( ph  \/  ps )  ->  ( -.  () ph 
->  () ps ) )
76orrd 367 . 2  |-  ( () ( ph  \/  ps )  ->  ( () ph  \/  () ps ) )
8 orc 374 . . . 4  |-  ( ph  ->  ( ph  \/  ps ) )
98impxt 25086 . . 3  |-  ( ()
ph  ->  () ( ph  \/  ps ) )
10 olc 373 . . . 4  |-  ( ps 
->  ( ph  \/  ps ) )
1110impxt 25086 . . 3  |-  ( () ps  ->  () ( ph  \/  ps ) )
129, 11jaoi 368 . 2  |-  ( ( () ph  \/  () ps )  ->  () (
ph  \/  ps )
)
137, 12impbii 180 1  |-  ( () ( ph  \/  ps ) 
<->  ( () ph  \/  () ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357   ()wcirc 25075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ltl2 25078  ax-ltl3 25079  ax-nmp 25082
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator