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

Theorem alrimiv 1799
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alrimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimiv  |-  ( ph  ->  A. x ps )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem alrimiv
StepHypRef Expression
1 ax-17 1462 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1401 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1379  ax-gen 1381  ax-17 1462
This theorem is referenced by:  alrimivv  1800  nfdv  1802  axext4  2069  eqrdv  2083  abbi2dv  2203  abbi1dv  2204  elex22  2628  elex2  2629  spcimdv  2696  spcimedv  2698  pm13.183  2745  sbcthdv  2843  sbcimdv  2893  ssrdv  3020  ss2abdv  3083  abssdv  3084  opprc  3626  dfnfc2  3654  intss  3692  intab  3700  dfiin2g  3746  disjss1  3807  mpteq12dva  3894  el  3988  exmid0el  4007  exmidundif  4009  euotd  4055  reusv1  4254  elirr  4330  sucprcreg  4338  en2lp  4343  tfisi  4375  ssrelrel  4506  issref  4781  iotaval  4957  iota5  4966  iotabidv  4967  funmo  4996  funco  5019  funun  5023  fununi  5047  funcnvuni  5048  funimaexglem  5062  fvssunirng  5283  relfvssunirn  5284  sefvex  5289  nfunsn  5301  f1oresrab  5426  funoprabg  5701  mpt2fvex  5930  1stconst  5943  2ndconst  5944  tfrexlem  6053  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemaccex  6080  tfrcllemres  6081  tfrcl  6083  rdgexggg  6096  rdgifnon  6098  rdgifnon2  6099  rdgivallem  6100  frecabcl  6118  frectfr  6119  frecrdg  6127  iserd  6270  exmidpw  6576  fisseneq  6592  sbthlemi3  6612  finomni  6740  exmidomniim  6741  exmidomni  6742  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  pitonn  7329  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  zfz1iso  10143  shftfn  10155  2spim  11112  decidr  11141  bj-om  11277  bj-nnord  11298  bj-inf2vn  11314  bj-inf2vn2  11315  bj-findis  11319  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator