Theorem alrimiv 1872

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 1524	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1467	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 1445  ax-gen 1447  ax-17 1524

This theorem is referenced by:  alrimivv  1873  nfdv  1875  cbvalvw  1917  axext4  2159  eqrdv  2173  abbi2dv  2294  abbi1dv  2295  elex22  2750  elex2  2751  spcimdv  2819  spcimedv  2821  pm13.183  2873  sbcthdv  2975  sbcimdv  3026  ssrdv  3159  ss2abdv  3226  abssdv  3227  opprc  3795  dfnfc2  3823  intss  3861  intab  3869  dfiin2g  3915  disjss1  3981  mpteq12dva  4079  el  4173  exmid1dc  4195  exmidn0m  4196  exmid0el  4199  exmidundif  4201  exmidundifim  4202  euotd  4248  reusv1  4452  elirr  4534  sucprcreg  4542  en2lp  4547  tfisi  4580  ssrelrel  4720  issref  5003  iotaval  5181  iota5  5190  iotabidv  5191  funmo  5223  funco  5248  funun  5252  fununi  5276  funcnvuni  5277  funimaexglem  5291  fvssunirng  5522  relfvssunirn  5523  sefvex  5528  nfunsn  5541  f1oresrab  5673  funoprabg  5964  mpofvex  6194  1stconst  6212  2ndconst  6213  disjxp1  6227  tfrexlem  6325  tfr1onlemsucfn  6331  tfr1onlemsucaccv  6332  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfr1onlemaccex  6339  tfr1onlemres  6340  tfrcllemsucfn  6344  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllembfn  6348  tfrcllemaccex  6352  tfrcllemres  6353  tfrcl  6355  rdgexggg  6368  rdgifnon  6370  rdgifnon2  6371  rdgivallem  6372  frecabcl  6390  frectfr  6391  frecrdg  6399  iserd  6551  exmidpw  6898  exmidpweq  6899  fiintim  6918  fisseneq  6921  sbthlemi3  6948  finomni  7128  exmidomniim  7129  exmidomni  7130  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  cc1  7239  pitonn  7822  frecuzrdgtcl  10380  frecuzrdgfunlem  10387  zfz1iso  10787  shftfn  10799  exmidunben  12392  tgcl  13115  epttop  13141  neissex  13216  uptx  13325  dvfgg  13708  2spim  14058  decidr  14088  bj-om  14229  bj-nnord  14250  bj-inf2vn  14266  bj-inf2vn2  14267  bj-findis  14271  exmid1stab  14290  exmidsbthrlem  14311  sbthom  14315