Theorem alrimi 1568

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

Syntax hints:   -> wi 4   A.wal 1393   F/wnf 1506

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

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

This theorem is referenced by:  axc4i  1588  19.32r  1726  cbv3  1788  sbbid  1892  sbalyz  2050  dvelimdf  2067  dvelimor  2069  nf5d  2076  abbid  2346  nfcd  2367  nfabdw  2391  ralrimi  2601  r19.32r  2677  ceqsalg  2828  ceqsex  2838  vtocldf  2852  elrab3t  2958  morex  2987  sbciedf  3064  csbiebt  3164  csbiedf  3165  ssrd  3229  invdisj  4076  ssopab2b  4365  eusv2nf  4547  sniota  5309  imadif  5401  funimaexglem  5404  eusvobj1  5988  ssoprab2b  6061  ovmpodxf  6130  nninfinf  10665