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  2011  dvelimdf  2028  dvelimor  2030  nf5d  2037  abbid  2306  nfcd  2327  nfabdw  2351  ralrimi  2561  r19.32r  2636  ceqsalg  2780  ceqsex  2790  vtocldf  2803  elrab3t  2907  morex  2936  sbciedf  3013  csbiebt  3111  csbiedf  3112  ssrd  3175  rgenm  3540  invdisj  4012  ssopab2b  4294  eusv2nf  4474  sniota  5226  imadif  5315  funimaexglem  5318  eusvobj1  5883  ssoprab2b  5953  ovmpodxf  6022