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  3516  invdisj  3981  ssopab2b  4259  eusv2nf  4439  sniota  5187  imadif  5276  funimaexglem  5279  eusvobj1  5837  ssoprab2b  5907  ovmpodxf  5975
  Copyright terms: Public domain W3C validator