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

Theorem alrimih 1445
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 1431 . 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 1329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425
This theorem is referenced by:  albidh  1456  alrimi  1502  nfd  1503  19.21h  1536  exlimd2  1574  exlimdh  1575  eximdh  1590  nexd  1592  exbidh  1593  hbex  1615  hbnd  1633  19.12  1643  19.38  1654  ax11i  1692  equsalh  1704  nfald  1733  nfexd  1734  aev  1784  equs5or  1802  sb4or  1805  sbbidh  1817  sb6rf  1825  alrimiv  1846  eupicka  2077  2moex  2083
  Copyright terms: Public domain W3C validator