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

Theorem alrimih 1399
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 1385 . 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 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1377  ax-gen 1379
This theorem is referenced by:  albidh  1410  alrimi  1456  nfd  1457  19.21h  1490  exlimd2  1527  exlimdh  1528  eximdh  1543  nexd  1545  exbidh  1546  hbex  1568  hbnd  1586  19.12  1596  19.38  1607  ax11i  1643  equsalh  1655  nfald  1684  nfexd  1685  aev  1734  equs5or  1752  sb4or  1755  sbbidh  1767  sb6rf  1775  alrimiv  1796  eupicka  2022  2moex  2028
  Copyright terms: Public domain W3C validator