Theorem alrimi 1570

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

Syntax hints:   -> wi 4   A.wal 1395   F/wnf 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-4 1558

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

This theorem is referenced by:  axc4i  1590  19.32r  1727  cbv3  1789  sbbid  1893  sbalyz  2051  dvelimdf  2068  dvelimor  2070  nf5d  2077  abbid  2347  nfcd  2368  nfabdw  2392  ralrimi  2602  r19.32r  2678  ceqsalg  2830  ceqsex  2840  vtocldf  2854  elrab3t  2960  morex  2989  sbciedf  3066  csbiebt  3166  csbiedf  3167  ssrd  3231  invdisj  4082  ssopab2b  4373  eusv2nf  4555  sniota  5319  imadif  5412  funimaexglem  5415  eusvobj1  6010  ssoprab2b  6083  ovmpodxf  6152  modom  6999  nninfinf  10711