Theorem alrimiv 1754

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

Syntax hints:   -> wi 4   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1336  ax-gen 1338  ax-17 1419

This theorem is referenced by:  alrimivv  1755  nfdv  1757  axext4  2024  eqrdv  2038  abbi2dv  2156  abbi1dv  2157  elex22  2569  elex2  2570  spcimdv  2637  spcimedv  2639  pm13.183  2681  sbcthdv  2778  sbcimdv  2823  ssrdv  2951  ss2abdv  3013  abssdv  3014  opprc  3570  dfnfc2  3598  intss  3636  intab  3644  dfiin2g  3690  disjss1  3751  mpteq12dva  3838  el  3931  euotd  3991  reusv1  4190  elirr  4266  sucprcreg  4273  en2lp  4278  tfisi  4310  ssrelrel  4440  issref  4707  iotaval  4878  iota5  4887  iotabidv  4888  funmo  4917  funco  4940  funun  4944  fununi  4967  funcnvuni  4968  funimaexglem  4982  fvssunirng  5190  relfvssunirn  5191  sefvex  5196  nfunsn  5207  f1oresrab  5329  funoprabg  5600  mpt2fvex  5829  1stconst  5842  2ndconst  5843  tfrexlem  5948  rdgexggg  5964  rdgifnon  5966  rdgifnon2  5967  rdgivallem  5968  frectfr  5985  frecrdg  5992  iserd  6132  pitonn  6924  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdgfn  9198  frecuzrdgsuc  9201  shftfn  9425  2spim  9906  bj-om  10061  bj-nnord  10083  bj-inf2vn  10099  bj-inf2vn2  10100  bj-findis  10104