Theorem alrimiv 1862

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

Step	Hyp	Ref	Expression
1		ax-17 1514	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1457	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1435  ax-gen 1437  ax-17 1514

This theorem is referenced by:  alrimivv  1863  nfdv  1865  cbvalvw  1907  axext4  2149  eqrdv  2163  abbi2dv  2285  abbi1dv  2286  elex22  2741  elex2  2742  spcimdv  2810  spcimedv  2812  pm13.183  2864  sbcthdv  2965  sbcimdv  3016  ssrdv  3148  ss2abdv  3215  abssdv  3216  opprc  3779  dfnfc2  3807  intss  3845  intab  3853  dfiin2g  3899  disjss1  3965  mpteq12dva  4063  el  4157  exmid1dc  4179  exmidn0m  4180  exmid0el  4183  exmidundif  4185  exmidundifim  4186  euotd  4232  reusv1  4436  elirr  4518  sucprcreg  4526  en2lp  4531  tfisi  4564  ssrelrel  4704  issref  4986  iotaval  5164  iota5  5173  iotabidv  5174  funmo  5203  funco  5228  funun  5232  fununi  5256  funcnvuni  5257  funimaexglem  5271  fvssunirng  5501  relfvssunirn  5502  sefvex  5507  nfunsn  5520  f1oresrab  5650  funoprabg  5941  mpofvex  6171  1stconst  6189  2ndconst  6190  disjxp1  6204  tfrexlem  6302  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemaccex  6329  tfrcllemres  6330  tfrcl  6332  rdgexggg  6345  rdgifnon  6347  rdgifnon2  6348  rdgivallem  6349  frecabcl  6367  frectfr  6368  frecrdg  6376  iserd  6527  exmidpw  6874  exmidpweq  6875  fiintim  6894  fisseneq  6897  sbthlemi3  6924  finomni  7104  exmidomniim  7105  exmidomni  7106  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  cc1  7206  pitonn  7789  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  zfz1iso  10754  shftfn  10766  exmidunben  12359  tgcl  12704  epttop  12730  neissex  12805  uptx  12914  dvfgg  13297  2spim  13647  decidr  13677  bj-om  13819  bj-nnord  13840  bj-inf2vn  13856  bj-inf2vn2  13857  bj-findis  13861  exmid1stab  13880  exmidsbthrlem  13901  sbthom  13905