Theorem alrimi 1502

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

Syntax hints:   -> wi 4   A.wal 1329   F/wnf 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1423  ax-gen 1425  ax-4 1487

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

This theorem is referenced by:  19.32r  1658  cbv3  1720  sbbid  1818  sbalyz  1974  dvelimdf  1991  dvelimor  1993  abbid  2256  nfcd  2276  ralrimi  2503  r19.32r  2578  ceqsalg  2714  ceqsex  2724  vtocldf  2737  elrab3t  2839  morex  2868  sbciedf  2944  csbiebt  3039  csbiedf  3040  ssrd  3102  rgenm  3465  invdisj  3923  ssopab2b  4198  eusv2nf  4377  sniota  5115  imadif  5203  funimaexglem  5206  eusvobj1  5761  ssoprab2b  5828  ovmpodxf  5896