Theorem alrimi 1455

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

Syntax hints:   -> wi 4   A.wal 1282   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-5 1376  ax-gen 1378  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  19.32r  1610  cbv3  1670  sbbid  1767  sbalyz  1916  dvelimdf  1933  dvelimor  1935  abbid  2195  nfcd  2214  ralrimi  2432  r19.32r  2501  ceqsalg  2627  ceqsex  2637  vtocldf  2650  elrab3t  2748  morex  2776  sbciedf  2849  csbiebt  2942  csbiedf  2943  ssrd  3004  rgenm  3343  invdisj  3780  ssopab2b  4031  eusv2nf  4206  sniota  4914  imadif  4999  funimaexglem  5002  eusvobj1  5519  ssoprab2b  5582  ovmpt2dxf  5646