Theorem alrimiv 1795

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

Syntax hints:   -> wi 4   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1376  ax-gen 1378  ax-17 1459

This theorem is referenced by:  alrimivv  1796  nfdv  1798  axext4  2065  eqrdv  2079  abbi2dv  2197  abbi1dv  2198  elex22  2614  elex2  2615  spcimdv  2682  spcimedv  2684  pm13.183  2732  sbcthdv  2829  sbcimdv  2879  ssrdv  3005  ss2abdv  3067  abssdv  3068  opprc  3591  dfnfc2  3619  intss  3657  intab  3665  dfiin2g  3711  disjss1  3772  mpteq12dva  3859  el  3952  euotd  4009  reusv1  4208  elirr  4284  sucprcreg  4292  en2lp  4297  tfisi  4328  ssrelrel  4458  issref  4727  iotaval  4898  iota5  4907  iotabidv  4908  funmo  4937  funco  4960  funun  4964  fununi  4987  funcnvuni  4988  funimaexglem  5002  fvssunirng  5210  relfvssunirn  5211  sefvex  5216  nfunsn  5228  f1oresrab  5350  funoprabg  5620  mpt2fvex  5849  1stconst  5862  2ndconst  5863  tfrexlem  5971  rdgexggg  5987  rdgifnon  5989  rdgifnon2  5990  rdgivallem  5991  frectfr  6008  frecrdg  6015  iserd  6155  pitonn  7016  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgrom  9412  frecuzrdgfn  9414  frecuzrdgsuc  9417  shftfn  9712  2spim  10577  bj-om  10732  bj-nnord  10753  bj-inf2vn  10769  bj-inf2vn2  10770  bj-findis  10774