Theorem alrimiv 1888

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

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1461  ax-gen 1463  ax-17 1540

This theorem is referenced by:  alrimivv  1889  nfdv  1891  sbbidv  1899  cbvalvw  1934  axext4  2180  eqrdv  2194  abbi2dv  2315  abbi1dv  2316  elex22  2778  elex2  2779  spcimdv  2848  spcimedv  2850  pm13.183  2902  sbcthdv  3004  sbcimdv  3055  ssrdv  3190  ss2abdv  3257  abssdv  3258  opprc  3830  dfnfc2  3858  intss  3896  intab  3904  dfiin2g  3950  disjss1  4017  mpteq12dva  4115  el  4212  exmid1dc  4234  exmidn0m  4235  exmid0el  4238  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  euotd  4288  reusv1  4494  elirr  4578  sucprcreg  4586  en2lp  4591  tfisi  4624  ssrelrel  4764  issref  5053  iotaval  5231  iota5  5241  iotabidv  5242  funmo  5274  funco  5299  funun  5303  fununi  5327  funcnvuni  5328  funimaexglem  5342  fvssunirng  5576  relfvssunirn  5577  sefvex  5582  nfunsn  5596  f1oresrab  5730  funoprabg  6025  uchoice  6204  mpofvex  6272  1stconst  6288  2ndconst  6289  disjxp1  6303  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgexggg  6444  rdgifnon  6446  rdgifnon2  6447  rdgivallem  6448  frecabcl  6466  frectfr  6467  frecrdg  6475  iserd  6627  exmidpw  6978  exmidpweq  6979  exmidpw2en  6982  fiintim  7001  fisseneq  7004  sbthlemi3  7034  finomni  7215  exmidomniim  7216  exmidomni  7217  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidmotap  7344  cc1  7348  pitonn  7932  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  zfz1iso  10950  shftfn  11006  exmidunben  12668  prdsex  12971  imasex  13007  imasaddfnlemg  13016  lssex  13986  tgcl  14384  epttop  14410  neissex  14485  uptx  14594  dvfgg  15008  2spim  15496  decidr  15526  bj-om  15667  bj-nnord  15688  bj-inf2vn  15704  bj-inf2vn2  15705  bj-findis  15709  exmidsbthrlem  15753  sbthom  15757