Theorem alrimi 1522

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 1519	. 2 |- ( ph -> A. x ph )
3		alrimi.2	. 2 |- ( ph -> ps )
4	2, 3	alrimih 1469	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1351   F/wnf 1460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-4 1510

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

This theorem is referenced by:  axc4i  1542  19.32r  1680  cbv3  1742  sbbid  1846  sbalyz  1999  dvelimdf  2016  dvelimor  2018  nf5d  2025  abbid  2294  nfcd  2314  nfabdw  2338  ralrimi  2548  r19.32r  2623  ceqsalg  2765  ceqsex  2775  vtocldf  2788  elrab3t  2892  morex  2921  sbciedf  2998  csbiebt  3096  csbiedf  3097  ssrd  3160  rgenm  3525  invdisj  3997  ssopab2b  4276  eusv2nf  4456  sniota  5207  imadif  5296  funimaexglem  5299  eusvobj1  5861  ssoprab2b  5931  ovmpodxf  5999