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

Theorem alrimi 1458
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 1455 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1401 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285   F/wnf 1392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1379  ax-gen 1381  ax-4 1443
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  19.32r  1613  cbv3  1674  sbbid  1771  sbalyz  1920  dvelimdf  1937  dvelimor  1939  abbid  2201  nfcd  2220  ralrimi  2440  r19.32r  2510  ceqsalg  2641  ceqsex  2651  vtocldf  2664  elrab3t  2761  morex  2790  sbciedf  2863  csbiebt  2956  csbiedf  2957  ssrd  3019  rgenm  3371  invdisj  3815  ssopab2b  4077  eusv2nf  4252  sniota  4973  imadif  5059  funimaexglem  5062  eusvobj1  5600  ssoprab2b  5663  ovmpt2dxf  5727
  Copyright terms: Public domain W3C validator