Theorem alrimi 1545

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

Syntax hints:   -> wi 4   A.wal 1371   F/wnf 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1470  ax-gen 1472  ax-4 1533

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

This theorem is referenced by:  axc4i  1565  19.32r  1703  cbv3  1765  sbbid  1869  sbalyz  2027  dvelimdf  2044  dvelimor  2046  nf5d  2053  abbid  2322  nfcd  2343  nfabdw  2367  ralrimi  2577  r19.32r  2652  ceqsalg  2800  ceqsex  2810  vtocldf  2824  elrab3t  2928  morex  2957  sbciedf  3034  csbiebt  3133  csbiedf  3134  ssrd  3198  invdisj  4038  ssopab2b  4324  eusv2nf  4504  sniota  5263  imadif  5355  funimaexglem  5358  eusvobj1  5933  ssoprab2b  6004  ovmpodxf  6073  nninfinf  10590