Theorem alrimiv 1826

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

Syntax hints:   -> wi 4   A.wal 1310

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1404  ax-gen 1406  ax-17 1487

This theorem is referenced by:  alrimivv  1827  nfdv  1829  axext4  2097  eqrdv  2111  abbi2dv  2231  abbi1dv  2232  elex22  2670  elex2  2671  spcimdv  2739  spcimedv  2741  pm13.183  2790  sbcthdv  2890  sbcimdv  2940  ssrdv  3067  ss2abdv  3134  abssdv  3135  opprc  3690  dfnfc2  3718  intss  3756  intab  3764  dfiin2g  3810  disjss1  3876  mpteq12dva  3967  el  4060  exmid1dc  4081  exmidn0m  4082  exmid0el  4085  exmidundif  4087  exmidundifim  4088  euotd  4134  reusv1  4337  elirr  4414  sucprcreg  4422  en2lp  4427  tfisi  4459  ssrelrel  4597  issref  4877  iotaval  5055  iota5  5064  iotabidv  5065  funmo  5094  funco  5119  funun  5123  fununi  5147  funcnvuni  5148  funimaexglem  5162  fvssunirng  5388  relfvssunirn  5389  sefvex  5394  nfunsn  5407  f1oresrab  5537  funoprabg  5822  mpofvex  6052  1stconst  6069  2ndconst  6070  disjxp1  6084  tfrexlem  6182  tfr1onlemsucfn  6188  tfr1onlemsucaccv  6189  tfr1onlembxssdm  6191  tfr1onlembfn  6192  tfr1onlemaccex  6196  tfr1onlemres  6197  tfrcllemsucfn  6201  tfrcllemsucaccv  6202  tfrcllembxssdm  6204  tfrcllembfn  6205  tfrcllemaccex  6209  tfrcllemres  6210  tfrcl  6212  rdgexggg  6225  rdgifnon  6227  rdgifnon2  6228  rdgivallem  6229  frecabcl  6247  frectfr  6248  frecrdg  6256  iserd  6406  exmidpw  6752  fiintim  6767  fisseneq  6770  sbthlemi3  6796  finomni  6959  exmidomniim  6960  exmidomni  6961  exmidfodomrlemr  7002  exmidfodomrlemrALT  7003  pitonn  7576  frecuzrdgtcl  10071  frecuzrdgfunlem  10078  zfz1iso  10470  shftfn  10482  exmidunben  11777  tgcl  12069  epttop  12095  neissex  12170  uptx  12278  dvfgg  12605  2spim  12653  decidr  12682  bj-om  12814  bj-nnord  12835  bj-inf2vn  12851  bj-inf2vn2  12852  bj-findis  12856  exmidsbthrlem  12894  sbthom  12898