Theorem alrimiv 1867

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

Syntax hints:   -> wi 4   A.wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-17 1519

This theorem is referenced by:  alrimivv  1868  nfdv  1870  cbvalvw  1912  axext4  2154  eqrdv  2168  abbi2dv  2289  abbi1dv  2290  elex22  2745  elex2  2746  spcimdv  2814  spcimedv  2816  pm13.183  2868  sbcthdv  2969  sbcimdv  3020  ssrdv  3153  ss2abdv  3220  abssdv  3221  opprc  3786  dfnfc2  3814  intss  3852  intab  3860  dfiin2g  3906  disjss1  3972  mpteq12dva  4070  el  4164  exmid1dc  4186  exmidn0m  4187  exmid0el  4190  exmidundif  4192  exmidundifim  4193  euotd  4239  reusv1  4443  elirr  4525  sucprcreg  4533  en2lp  4538  tfisi  4571  ssrelrel  4711  issref  4993  iotaval  5171  iota5  5180  iotabidv  5181  funmo  5213  funco  5238  funun  5242  fununi  5266  funcnvuni  5267  funimaexglem  5281  fvssunirng  5511  relfvssunirn  5512  sefvex  5517  nfunsn  5530  f1oresrab  5661  funoprabg  5952  mpofvex  6182  1stconst  6200  2ndconst  6201  disjxp1  6215  tfrexlem  6313  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  rdgexggg  6356  rdgifnon  6358  rdgifnon2  6359  rdgivallem  6360  frecabcl  6378  frectfr  6379  frecrdg  6387  iserd  6539  exmidpw  6886  exmidpweq  6887  fiintim  6906  fisseneq  6909  sbthlemi3  6936  finomni  7116  exmidomniim  7117  exmidomni  7118  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  cc1  7227  pitonn  7810  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  zfz1iso  10776  shftfn  10788  exmidunben  12381  tgcl  12858  epttop  12884  neissex  12959  uptx  13068  dvfgg  13451  2spim  13801  decidr  13831  bj-om  13972  bj-nnord  13993  bj-inf2vn  14009  bj-inf2vn2  14010  bj-findis  14014  exmid1stab  14033  exmidsbthrlem  14054  sbthom  14058