Theorem alrimiv 1923

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

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  alrimivv  1924  nfdv  1926  sbbidv  1934  cbvalvw  1969  axext4  2216  eqrdv  2230  abbi2dv  2353  abbi1dv  2354  elex22  2828  elex2  2829  spcimdv  2900  spcimedv  2902  pm13.183  2954  sbcthdv  3056  sbcimdv  3107  ssrdv  3243  ss2abdv  3310  abssdv  3311  opprc  3903  dfnfc2  3931  intss  3969  intab  3977  dfiin2g  4023  disjss1  4090  mpteq12dva  4190  el  4290  exmid1dc  4312  exmidn0m  4313  exmid0el  4316  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  euotd  4370  reusv1  4578  elirr  4662  sucprcreg  4670  en2lp  4675  tfisi  4708  ssrelrel  4849  issref  5144  iotaval  5323  iota5  5333  iotabidv  5334  funmo  5366  funco  5391  funun  5396  fununfun  5398  fununi  5423  funcnvuni  5424  funimaexglem  5438  fvssunirng  5684  relfvssunirn  5685  sefvex  5690  nfunsn  5706  f1oresrab  5841  funoprabg  6151  uchoice  6330  mpofvex  6400  1stconst  6416  2ndconst  6417  disjxp1  6431  tfrexlem  6564  tfr1onlemsucfn  6570  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlembfn  6574  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllemsucfn  6583  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllembfn  6587  tfrcllemaccex  6591  tfrcllemres  6592  tfrcl  6594  rdgexggg  6607  rdgifnon  6609  rdgifnon2  6610  rdgivallem  6611  frecabcl  6629  frectfr  6630  frecrdg  6638  iserd  6792  modom  7060  exmidpw  7167  exmidpweq  7168  exmidpw2en  7171  fiintim  7190  fisseneq  7194  sbthlemi3  7228  finomni  7430  exmidomniim  7431  exmidomni  7432  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidmotap  7574  cc1  7578  pitonn  8162  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  zfz1iso  11209  shftfn  11505  exmidunben  13169  prdsex  13474  imasex  13510  imasaddfnlemg  13519  lssex  14494  tgcl  14921  epttop  14947  neissex  15022  uptx  15131  dvfgg  15545  upgrspanop  16270  umgrspanop  16271  usgrspanop  16272  2spim  16530  decidr  16560  bj-om  16699  bj-nnord  16720  bj-inf2vn  16736  bj-inf2vn2  16737  bj-findis  16741  exmidsbthrlem  16794  sbthom  16798