Theorem alrimi 1533

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-4 1521

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

This theorem is referenced by:  axc4i  1553  19.32r  1691  cbv3  1753  sbbid  1857  sbalyz  2015  dvelimdf  2032  dvelimor  2034  nf5d  2041  abbid  2310  nfcd  2331  nfabdw  2355  ralrimi  2565  r19.32r  2640  ceqsalg  2788  ceqsex  2798  vtocldf  2812  elrab3t  2916  morex  2945  sbciedf  3022  csbiebt  3121  csbiedf  3122  ssrd  3185  invdisj  4024  ssopab2b  4308  eusv2nf  4488  sniota  5246  imadif  5335  funimaexglem  5338  eusvobj1  5906  ssoprab2b  5976  ovmpodxf  6045  nninfinf  10517