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

Theorem alrimiv 1770
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 1435 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1374 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1352  ax-gen 1354  ax-17 1435
This theorem is referenced by:  alrimivv  1771  nfdv  1773  axext4  2040  eqrdv  2054  abbi2dv  2172  abbi1dv  2173  elex22  2586  elex2  2587  spcimdv  2654  spcimedv  2656  pm13.183  2704  sbcthdv  2801  sbcimdv  2851  ssrdv  2979  ss2abdv  3041  abssdv  3042  opprc  3598  dfnfc2  3626  intss  3664  intab  3672  dfiin2g  3718  disjss1  3779  mpteq12dva  3866  el  3959  euotd  4019  reusv1  4218  elirr  4294  sucprcreg  4301  en2lp  4306  tfisi  4338  ssrelrel  4468  issref  4735  iotaval  4906  iota5  4915  iotabidv  4916  funmo  4945  funco  4968  funun  4972  fununi  4995  funcnvuni  4996  funimaexglem  5010  fvssunirng  5218  relfvssunirn  5219  sefvex  5224  nfunsn  5235  f1oresrab  5357  funoprabg  5628  mpt2fvex  5857  1stconst  5870  2ndconst  5871  tfrexlem  5979  rdgexggg  5995  rdgifnon  5997  rdgifnon2  5998  rdgivallem  5999  frectfr  6016  frecrdg  6023  iserd  6163  pitonn  6982  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgrom  9360  frecuzrdgfn  9362  frecuzrdgsuc  9365  shftfn  9653  2spim  10293  bj-om  10448  bj-nnord  10470  bj-inf2vn  10486  bj-inf2vn2  10487  bj-findis  10491
  Copyright terms: Public domain W3C validator