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

Theorem alrimih 1403
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 1389 . 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 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1381  ax-gen 1383
This theorem is referenced by:  albidh  1414  alrimi  1460  nfd  1461  19.21h  1494  exlimd2  1531  exlimdh  1532  eximdh  1547  nexd  1549  exbidh  1550  hbex  1572  hbnd  1590  19.12  1600  19.38  1611  ax11i  1649  equsalh  1661  nfald  1690  nfexd  1691  aev  1740  equs5or  1758  sb4or  1761  sbbidh  1773  sb6rf  1781  alrimiv  1802  eupicka  2028  2moex  2034
  Copyright terms: Public domain W3C validator