MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hbim Unicode version

Theorem hbim 1737
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  ->  ps ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.)
Hypotheses
Ref Expression
hbim.1  |-  ( ph  ->  A. x ph )
hbim.2  |-  ( ps 
->  A. x ps )
Assertion
Ref Expression
hbim  |-  ( (
ph  ->  ps )  ->  A. x ( ph  ->  ps ) )

Proof of Theorem hbim
StepHypRef Expression
1 hbim.1 . . . 4  |-  ( ph  ->  A. x ph )
21hbn 1732 . . 3  |-  ( -. 
ph  ->  A. x  -.  ph )
3 pm2.21 100 . . 3  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
42, 3alrimih 1555 . 2  |-  ( -. 
ph  ->  A. x ( ph  ->  ps ) )
5 hbim.2 . . 3  |-  ( ps 
->  A. x ps )
6 ax-1 5 . . 3  |-  ( ps 
->  ( ph  ->  ps ) )
75, 6alrimih 1555 . 2  |-  ( ps 
->  A. x ( ph  ->  ps ) )
84, 7ja 153 1  |-  ( (
ph  ->  ps )  ->  A. x ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1530
This theorem is referenced by:  19.23h  1740  19.21h  1743  hban  1748  cbv3hv  1749  ax12olem5  1884  cleqh  2393  hbral  2604  cbv3hvNEW7  29423  ax12OLD  29727  a12study9  29742  a12study5rev  29744  a12study10  29758  a12study10n  29759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
  Copyright terms: Public domain W3C validator