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

Theorem alrimi 1470
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 1467 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1413 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1297   F/wnf 1404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1391  ax-gen 1393  ax-4 1455
This theorem depends on definitions:  df-bi 116  df-nf 1405
This theorem is referenced by:  19.32r  1626  cbv3  1688  sbbid  1785  sbalyz  1935  dvelimdf  1952  dvelimor  1954  abbid  2216  nfcd  2235  ralrimi  2462  r19.32r  2536  ceqsalg  2669  ceqsex  2679  vtocldf  2692  elrab3t  2792  morex  2821  sbciedf  2896  csbiebt  2989  csbiedf  2990  ssrd  3052  rgenm  3412  invdisj  3869  ssopab2b  4136  eusv2nf  4315  sniota  5051  imadif  5139  funimaexglem  5142  eusvobj1  5693  ssoprab2b  5760  ovmpodxf  5828
  Copyright terms: Public domain W3C validator