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

Theorem alrimi 1515
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 1512 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1462 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1346   F/wnf 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1440  ax-gen 1442  ax-4 1503
This theorem depends on definitions:  df-bi 116  df-nf 1454
This theorem is referenced by:  axc4i  1535  19.32r  1673  cbv3  1735  sbbid  1839  sbalyz  1992  dvelimdf  2009  dvelimor  2011  nf5d  2018  abbid  2287  nfcd  2307  nfabdw  2331  ralrimi  2541  r19.32r  2616  ceqsalg  2758  ceqsex  2768  vtocldf  2781  elrab3t  2885  morex  2914  sbciedf  2990  csbiebt  3088  csbiedf  3089  ssrd  3152  rgenm  3517  invdisj  3983  ssopab2b  4261  eusv2nf  4441  sniota  5189  imadif  5278  funimaexglem  5281  eusvobj1  5840  ssoprab2b  5910  ovmpodxf  5978
  Copyright terms: Public domain W3C validator