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

Theorem alrimih 1449
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 1435 . 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 1333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1427  ax-gen 1429
This theorem is referenced by:  albidh  1460  alrimi  1502  nfd  1503  19.21h  1537  exlimd2  1575  exlimdh  1576  eximdh  1591  nexd  1593  exbidh  1594  hbex  1616  hbnd  1635  19.12  1645  19.38  1656  ax11i  1694  equsalh  1706  nfald  1740  nfexd  1741  aev  1792  equs5or  1810  sb4or  1813  sbbidh  1825  sb6rf  1833  alrimiv  1854  eupicka  2086  2moex  2092
  Copyright terms: Public domain W3C validator