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

Axiom ax-ltl3 25079
Description: If, in the next step,  ph  ->  ps and  ph hold then, in the next step,  ps holds. (Contributed by FL, 20-Mar-2011.)
Assertion
Ref Expression
ax-ltl3  |-  ( () ( ph  ->  ps )  ->  ( () ph  ->  () ps ) )

Detailed syntax breakdown of Axiom ax-ltl3
StepHypRef Expression
1 wph . . . 4  wff  ph
2 wps . . . 4  wff  ps
31, 2wi 4 . . 3  wff  ( ph  ->  ps )
43wcirc 25075 . 2  wff  () (
ph  ->  ps )
51wcirc 25075 . . 3  wff  () ph
62wcirc 25075 . . 3  wff  () ps
75, 6wi 4 . 2  wff  ( ()
ph  ->  () ps )
84, 7wi 4 1  wff  ( () ( ph  ->  ps )  ->  ( () ph  ->  () ps ) )
Colors of variables: wff set class
This axiom is referenced by:  impxt  25086  nxtor  25088  nxtand  25089  nxtimd  25112  untind  25121
  Copyright terms: Public domain W3C validator