Theorem alrimiv 1922

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

Syntax hints:   -> wi 4   A.wal 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1495  ax-gen 1497  ax-17 1574

This theorem is referenced by:  alrimivv  1923  nfdv  1925  sbbidv  1933  cbvalvw  1968  axext4  2215  eqrdv  2229  abbi2dv  2350  abbi1dv  2351  elex22  2818  elex2  2819  spcimdv  2890  spcimedv  2892  pm13.183  2944  sbcthdv  3046  sbcimdv  3097  ssrdv  3233  ss2abdv  3300  abssdv  3301  opprc  3883  dfnfc2  3911  intss  3949  intab  3957  dfiin2g  4003  disjss1  4070  mpteq12dva  4170  el  4268  exmid1dc  4290  exmidn0m  4291  exmid0el  4294  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  euotd  4347  reusv1  4555  elirr  4639  sucprcreg  4647  en2lp  4652  tfisi  4685  ssrelrel  4826  issref  5119  iotaval  5298  iota5  5308  iotabidv  5309  funmo  5341  funco  5366  funun  5371  fununfun  5373  fununi  5398  funcnvuni  5399  funimaexglem  5413  fvssunirng  5654  relfvssunirn  5655  sefvex  5660  nfunsn  5676  f1oresrab  5812  funoprabg  6119  uchoice  6299  mpofvex  6369  1stconst  6385  2ndconst  6386  disjxp1  6400  tfrexlem  6499  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  rdgexggg  6542  rdgifnon  6544  rdgifnon2  6545  rdgivallem  6546  frecabcl  6564  frectfr  6565  frecrdg  6573  iserd  6727  modom  6993  exmidpw  7099  exmidpweq  7100  exmidpw2en  7103  fiintim  7122  fisseneq  7126  sbthlemi3  7157  finomni  7338  exmidomniim  7339  exmidomni  7340  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidmotap  7479  cc1  7483  pitonn  8067  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  zfz1iso  11104  shftfn  11384  exmidunben  13046  prdsex  13351  imasex  13387  imasaddfnlemg  13396  lssex  14367  tgcl  14787  epttop  14813  neissex  14888  uptx  14997  dvfgg  15411  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  2spim  16362  decidr  16392  bj-om  16532  bj-nnord  16553  bj-inf2vn  16569  bj-inf2vn2  16570  bj-findis  16574  exmidsbthrlem  16626  sbthom  16630