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  2121  eqrdv  2135  abbi2dv  2256  abbi1dv  2257  elex22  2696  elex2  2697  spcimdv  2765  spcimedv  2767  pm13.183  2817  sbcthdv  2918  sbcimdv  2969  ssrdv  3098  ss2abdv  3165  abssdv  3166  opprc  3721  dfnfc2  3749  intss  3787  intab  3795  dfiin2g  3841  disjss1  3907  mpteq12dva  4004  el  4097  exmid1dc  4118  exmidn0m  4119  exmid0el  4122  exmidundif  4124  exmidundifim  4125  euotd  4171  reusv1  4374  elirr  4451  sucprcreg  4459  en2lp  4464  tfisi  4496  ssrelrel  4634  issref  4916  iotaval  5094  iota5  5103  iotabidv  5104  funmo  5133  funco  5158  funun  5162  fununi  5186  funcnvuni  5187  funimaexglem  5201  fvssunirng  5429  relfvssunirn  5430  sefvex  5435  nfunsn  5448  f1oresrab  5578  funoprabg  5863  mpofvex  6094  1stconst  6111  2ndconst  6112  disjxp1  6126  tfrexlem  6224  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  rdgexggg  6267  rdgifnon  6269  rdgifnon2  6270  rdgivallem  6271  frecabcl  6289  frectfr  6290  frecrdg  6298  iserd  6448  exmidpw  6795  fiintim  6810  fisseneq  6813  sbthlemi3  6840  finomni  7005  exmidomniim  7006  exmidomni  7007  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  pitonn  7649  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  zfz1iso  10577  shftfn  10589  exmidunben  11928  tgcl  12222  epttop  12248  neissex  12323  uptx  12432  dvfgg  12815  2spim  12962  decidr  12992  bj-om  13124  bj-nnord  13145  bj-inf2vn  13161  bj-inf2vn2  13162  bj-findis  13166  exmid1stab  13184  exmidsbthrlem  13206  sbthom  13210