ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimih Unicode version

Theorem exlimih 1527
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Hypotheses
Ref Expression
exlimih.1  |-  ( ps 
->  A. x ps )
exlimih.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimih  |-  ( E. x ph  ->  ps )

Proof of Theorem exlimih
StepHypRef Expression
1 exlimih.1 . . 3  |-  ( ps 
->  A. x ps )
2119.23h 1430 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimih.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1384 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285   E.wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1381  ax-ie2 1426
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exlimi  1528  exlimiv  1532  19.43  1562  hbex  1570  ax6blem  1583  19.41h  1618  ax9o  1631  equid  1632  equsex  1660  cbvexh  1682  equs5a  1719  sb5rf  1777  equvin  1788  euan  2001  moexexdc  2029
  Copyright terms: Public domain W3C validator