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

Theorem impbox 24981
Description: If  ph  ->  ps is unconditionally true and if  ph is always true then  ps is always true. (Contributed by FL, 22-Feb-2011.)
Hypothesis
Ref Expression
impbox.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
impbox  |-  ( [.] ph  ->  [.] ps )

Proof of Theorem impbox
StepHypRef Expression
1 impbox.1 . . 3  |-  ( ph  ->  ps )
21ax-lmp 24978 . 2  |-  [.] ( ph  ->  ps )
3 ax-ltl1 24974 . 2  |-  ( [.] ( ph  ->  ps )  ->  ( [.] ph  ->  [.] ps ) )
42, 3ax-mp 8 1  |-  ( [.] ph  ->  [.] ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   [.]wbox 24970
This theorem is referenced by:  bibox  24982  diaimi  24988  evpexun  24998  alalifal  25003  alneal1a  25004  impbox2  25005  boxand  25006  boxrim  25007
This theorem was proved from axioms:  ax-mp 8  ax-ltl1 24974  ax-lmp 24978
  Copyright terms: Public domain W3C validator