Theorem alrimi 1510

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

Syntax hints:   -> wi 4   A.wal 1341   F/wnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1435  ax-gen 1437  ax-4 1498

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  axc4i  1530  19.32r  1668  cbv3  1730  sbbid  1834  sbalyz  1987  dvelimdf  2004  dvelimor  2006  nf5d  2013  abbid  2283  nfcd  2303  nfabdw  2327  ralrimi  2537  r19.32r  2612  ceqsalg  2754  ceqsex  2764  vtocldf  2777  elrab3t  2881  morex  2910  sbciedf  2986  csbiebt  3084  csbiedf  3085  ssrd  3147  rgenm  3511  invdisj  3976  ssopab2b  4254  eusv2nf  4434  sniota  5180  imadif  5268  funimaexglem  5271  eusvobj1  5829  ssoprab2b  5899  ovmpodxf  5967