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

Theorem alrimi 1533
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1  |-  F/ x ph
alrimi.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimi  |-  ( ph  ->  A. x ps )

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3  |-  F/ x ph
21nfri 1530 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1480 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1362   F/wnf 1471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-4 1521
This theorem depends on definitions:  df-bi 117  df-nf 1472
This theorem is referenced by:  axc4i  1553  19.32r  1691  cbv3  1753  sbbid  1857  sbalyz  2011  dvelimdf  2028  dvelimor  2030  nf5d  2037  abbid  2306  nfcd  2327  nfabdw  2351  ralrimi  2561  r19.32r  2636  ceqsalg  2780  ceqsex  2790  vtocldf  2803  elrab3t  2907  morex  2936  sbciedf  3013  csbiebt  3111  csbiedf  3112  ssrd  3175  rgenm  3540  invdisj  4012  ssopab2b  4294  eusv2nf  4474  sniota  5226  imadif  5315  funimaexglem  5318  eusvobj1  5883  ssoprab2b  5953  ovmpodxf  6022
  Copyright terms: Public domain W3C validator