Theorem alrimi 1533

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1	|- F/ x ph
alrimi.2	|- ( ph -> ps )

Assertion

Ref	Expression
alrimi	|- ( ph -> A. x ps )

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3 |- F/ x ph
2	1	nfri 1530	. 2 |- ( ph -> A. x ph )
3		alrimi.2	. 2 |- ( ph -> ps )
4	2, 3	alrimih 1480	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  axc4i  1553  19.32r  1691  cbv3  1753  sbbid  1857  sbalyz  2015  dvelimdf  2032  dvelimor  2034  nf5d  2041  abbid  2310  nfcd  2331  nfabdw  2355  ralrimi  2565  r19.32r  2640  ceqsalg  2788  ceqsex  2798  vtocldf  2811  elrab3t  2915  morex  2944  sbciedf  3021  csbiebt  3120  csbiedf  3121  ssrd  3184  invdisj  4023  ssopab2b  4307  eusv2nf  4487  sniota  5245  imadif  5334  funimaexglem  5337  eusvobj1  5905  ssoprab2b  5975  ovmpodxf  6044  nninfinf  10514