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

Theorem alrimih 1462
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
Hypotheses
Ref Expression
alrimih.1  |-  ( ph  ->  A. x ph )
alrimih.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimih  |-  ( ph  ->  A. x ps )

Proof of Theorem alrimih
StepHypRef Expression
1 alrimih.1 . 2  |-  ( ph  ->  A. x ph )
2 alrimih.2 . . 3  |-  ( ph  ->  ps )
32alimi 1448 . 2  |-  ( A. x ph  ->  A. x ps )
41, 3syl 14 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442
This theorem is referenced by:  albidh  1473  alrimi  1515  nfd  1516  19.21h  1550  exlimd2  1588  exlimdh  1589  eximdh  1604  nexd  1606  exbidh  1607  hbex  1629  hbnd  1648  19.12  1658  19.38  1669  ax11i  1707  equsalh  1719  nfald  1753  nfexd  1754  aev  1805  equs5or  1823  sb4or  1826  sbbidh  1838  sb6rf  1846  alrimiv  1867  eupicka  2099  2moex  2105
  Copyright terms: Public domain W3C validator