Theorem alrimiv 1846

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

Syntax hints:   -> wi 4   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-17 1506

This theorem is referenced by:  alrimivv  1847  nfdv  1849  axext4  2123  eqrdv  2137  abbi2dv  2258  abbi1dv  2259  elex22  2701  elex2  2702  spcimdv  2770  spcimedv  2772  pm13.183  2822  sbcthdv  2923  sbcimdv  2974  ssrdv  3103  ss2abdv  3170  abssdv  3171  opprc  3726  dfnfc2  3754  intss  3792  intab  3800  dfiin2g  3846  disjss1  3912  mpteq12dva  4009  el  4102  exmid1dc  4123  exmidn0m  4124  exmid0el  4127  exmidundif  4129  exmidundifim  4130  euotd  4176  reusv1  4379  elirr  4456  sucprcreg  4464  en2lp  4469  tfisi  4501  ssrelrel  4639  issref  4921  iotaval  5099  iota5  5108  iotabidv  5109  funmo  5138  funco  5163  funun  5167  fununi  5191  funcnvuni  5192  funimaexglem  5206  fvssunirng  5436  relfvssunirn  5437  sefvex  5442  nfunsn  5455  f1oresrab  5585  funoprabg  5870  mpofvex  6101  1stconst  6118  2ndconst  6119  disjxp1  6133  tfrexlem  6231  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  rdgexggg  6274  rdgifnon  6276  rdgifnon2  6277  rdgivallem  6278  frecabcl  6296  frectfr  6297  frecrdg  6305  iserd  6455  exmidpw  6802  fiintim  6817  fisseneq  6820  sbthlemi3  6847  finomni  7012  exmidomniim  7013  exmidomni  7014  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  pitonn  7656  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  zfz1iso  10584  shftfn  10596  exmidunben  11939  tgcl  12233  epttop  12259  neissex  12334  uptx  12443  dvfgg  12826  2spim  12973  decidr  13003  bj-om  13135  bj-nnord  13156  bj-inf2vn  13172  bj-inf2vn2  13173  bj-findis  13177  exmid1stab  13195  exmidsbthrlem  13217  sbthom  13221