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  3188  invdisj  4027  ssopab2b  4311  eusv2nf  4491  sniota  5249  imadif  5338  funimaexglem  5341  eusvobj1  5909  ssoprab2b  5979  ovmpodxf  6048  nninfinf  10535