Theorem alrimiv 1927

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

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  alrimivv  1928  nfdv  1930  sbbidv  1939  cbvalvw  1975  axext4  2222  eqrdv  2236  abbi2dv  2359  abbi1dv  2360  elex22  2837  elex2  2838  spcimdv  2909  spcimedv  2911  pm13.183  2964  sbcthdv  3066  sbcimdv  3117  ssrdv  3254  ss2abdv  3321  abssdv  3322  opprc  3925  dfnfc2  3953  intss  3991  intab  3999  dfiin2g  4045  disjss1  4112  sn0disj  4127  mpteq12dva  4213  el  4317  exmid1dc  4339  exmidn0m  4340  exmid0el  4343  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  euotd  4397  reusv1  4606  elirr  4690  sucprcreg  4698  en2lp  4703  tfisi  4736  ssrelrel  4877  issref  5173  iotaval  5352  iota5  5362  iotabidv  5363  funmo  5395  funco  5420  funun  5425  fununfun  5427  fununi  5452  funcnvuni  5453  funimaexglem  5467  fvssunirng  5713  relfvssunirn  5714  sefvex  5719  nfunsn  5736  f1oresrab  5876  funoprabg  6190  uchoice  6375  mpofvex  6445  1stconst  6461  2ndconst  6462  disjxp1  6476  tfrexlem  6610  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  rdgexggg  6653  rdgifnon  6655  rdgifnon2  6656  rdgivallem  6657  frecabcl  6675  frectfr  6676  frecrdg  6684  iserd  6838  fsetdmprc0  6955  modom  7114  exmidpw  7221  exmidpweq  7222  exmidpw2en  7225  fiintim  7244  fisseneq  7248  sbthlemi3  7283  finomni  7486  exmidomniim  7487  exmidomni  7488  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidmotap  7633  cc1  7637  pitonn  8221  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  zfz1iso  11314  shftfn  11610  ballotfilem2  13285  exmidunben  13374  imasex  13684  imasaddfnlemg  13693  prdsex  14278  lssex  14799  tgcl  15307  epttop  15333  neissex  15408  uptx  15517  dvfgg  15931  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  2spim  17016  decidr  17046  bj-om  17185  bj-nnord  17206  bj-inf2vn  17222  bj-inf2vn2  17223  bj-findis  17227  exmidsbthrlem  17290  sbthom  17294