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  2767  ceqsex  2777  vtocldf  2790  elrab3t  2894  morex  2923  sbciedf  3000  csbiebt  3098  csbiedf  3099  ssrd  3162  rgenm  3527  invdisj  3999  ssopab2b  4278  eusv2nf  4458  sniota  5209  imadif  5298  funimaexglem  5301  eusvobj1  5864  ssoprab2b  5934  ovmpodxf  6002