Theorem alrimiv 1874

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 1526	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1469	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1447  ax-gen 1449  ax-17 1526

This theorem is referenced by:  alrimivv  1875  nfdv  1877  cbvalvw  1919  axext4  2161  eqrdv  2175  abbi2dv  2296  abbi1dv  2297  elex22  2753  elex2  2754  spcimdv  2822  spcimedv  2824  pm13.183  2876  sbcthdv  2978  sbcimdv  3029  ssrdv  3162  ss2abdv  3229  abssdv  3230  opprc  3800  dfnfc2  3828  intss  3866  intab  3874  dfiin2g  3920  disjss1  3987  mpteq12dva  4085  el  4179  exmid1dc  4201  exmidn0m  4202  exmid0el  4205  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  euotd  4255  reusv1  4459  elirr  4541  sucprcreg  4549  en2lp  4554  tfisi  4587  ssrelrel  4727  issref  5012  iotaval  5190  iota5  5199  iotabidv  5200  funmo  5232  funco  5257  funun  5261  fununi  5285  funcnvuni  5286  funimaexglem  5300  fvssunirng  5531  relfvssunirn  5532  sefvex  5537  nfunsn  5550  f1oresrab  5682  funoprabg  5974  mpofvex  6204  1stconst  6222  2ndconst  6223  disjxp1  6237  tfrexlem  6335  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  tfrcllemres  6363  tfrcl  6365  rdgexggg  6378  rdgifnon  6380  rdgifnon2  6381  rdgivallem  6382  frecabcl  6400  frectfr  6401  frecrdg  6409  iserd  6561  exmidpw  6908  exmidpweq  6909  fiintim  6928  fisseneq  6931  sbthlemi3  6958  finomni  7138  exmidomniim  7139  exmidomni  7140  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidmotap  7260  cc1  7264  pitonn  7847  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  zfz1iso  10821  shftfn  10833  exmidunben  12427  prdsex  12718  imasex  12726  imasaddfnlemg  12735  tgcl  13567  epttop  13593  neissex  13668  uptx  13777  dvfgg  14160  2spim  14521  decidr  14551  bj-om  14692  bj-nnord  14713  bj-inf2vn  14729  bj-inf2vn2  14730  bj-findis  14734  exmidsbthrlem  14773  sbthom  14777