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

Theorem alrimi 1456
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 1453 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1399 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283   F/wnf 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1377  ax-gen 1379  ax-4 1441
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  19.32r  1611  cbv3  1671  sbbid  1768  sbalyz  1917  dvelimdf  1934  dvelimor  1936  abbid  2196  nfcd  2215  ralrimi  2433  r19.32r  2502  ceqsalg  2628  ceqsex  2638  vtocldf  2651  elrab3t  2749  morex  2777  sbciedf  2850  csbiebt  2943  csbiedf  2944  ssrd  3005  rgenm  3351  invdisj  3788  ssopab2b  4039  eusv2nf  4214  sniota  4924  imadif  5010  funimaexglem  5013  eusvobj1  5530  ssoprab2b  5593  ovmpt2dxf  5657
  Copyright terms: Public domain W3C validator