Theorem alrimi 1470

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

Syntax hints:   -> wi 4   A.wal 1297   F/wnf 1404

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1391  ax-gen 1393  ax-4 1455

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

This theorem is referenced by:  19.32r  1626  cbv3  1688  sbbid  1785  sbalyz  1935  dvelimdf  1952  dvelimor  1954  abbid  2216  nfcd  2235  ralrimi  2462  r19.32r  2536  ceqsalg  2669  ceqsex  2679  vtocldf  2692  elrab3t  2792  morex  2821  sbciedf  2896  csbiebt  2989  csbiedf  2990  ssrd  3052  rgenm  3412  invdisj  3869  ssopab2b  4136  eusv2nf  4315  sniota  5051  imadif  5139  funimaexglem  5142  eusvobj1  5693  ssoprab2b  5760  ovmpodxf  5828