Theorem alrimi 1515

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

Syntax hints:   -> wi 4   A.wal 1346   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1440  ax-gen 1442  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  axc4i  1535  19.32r  1673  cbv3  1735  sbbid  1839  sbalyz  1992  dvelimdf  2009  dvelimor  2011  nf5d  2018  abbid  2287  nfcd  2307  nfabdw  2331  ralrimi  2541  r19.32r  2616  ceqsalg  2758  ceqsex  2768  vtocldf  2781  elrab3t  2885  morex  2914  sbciedf  2990  csbiebt  3088  csbiedf  3089  ssrd  3152  rgenm  3516  invdisj  3981  ssopab2b  4259  eusv2nf  4439  sniota  5187  imadif  5276  funimaexglem  5279  eusvobj1  5837  ssoprab2b  5907  ovmpodxf  5975