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

Theorem impbox 25084
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 25081 . 2  |-  [.] ( ph  ->  ps )
3 ax-ltl1 25077 . 2  |-  ( [.] ( ph  ->  ps )  ->  ( [.] ph  ->  [.] ps ) )
42, 3ax-mp 8 1  |-  ( [.] ph  ->  [.] ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   [.]wbox 25073
This theorem is referenced by:  bibox  25085  diaimi  25091  evpexun  25101  alalifal  25106  alneal1a  25107  impbox2  25108  boxand  25109  boxrim  25110
This theorem was proved from axioms:  ax-mp 8  ax-ltl1 25077  ax-lmp 25081
  Copyright terms: Public domain W3C validator