Theorem alrimi 1536

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

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1461  ax-gen 1463  ax-4 1524

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

This theorem is referenced by:  axc4i  1556  19.32r  1694  cbv3  1756  sbbid  1860  sbalyz  2018  dvelimdf  2035  dvelimor  2037  nf5d  2044  abbid  2313  nfcd  2334  nfabdw  2358  ralrimi  2568  r19.32r  2643  ceqsalg  2791  ceqsex  2801  vtocldf  2815  elrab3t  2919  morex  2948  sbciedf  3025  csbiebt  3124  csbiedf  3125  ssrd  3189  invdisj  4028  ssopab2b  4312  eusv2nf  4492  sniota  5250  imadif  5339  funimaexglem  5342  eusvobj1  5912  ssoprab2b  5983  ovmpodxf  6052  nninfinf  10552