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

Theorem exlimih 1525
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 1428 . 2  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
3 exlimih.2 . 2  |-  ( ph  ->  ps )
42, 3mpgbi 1382 1  |-  ( E. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exlimi  1526  exlimiv  1530  19.43  1560  hbex  1568  ax6blem  1581  19.41h  1616  ax9o  1629  equid  1630  equsex  1657  cbvexh  1679  equs5a  1716  sb5rf  1774  equvin  1785  euan  1998  moexexdc  2026
  Copyright terms: Public domain W3C validator