Theorem alrimi 1415

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

Syntax hints:   -> wi 4   A.wal 1241   F/wnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1336  ax-gen 1338  ax-4 1400

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  19.32r  1570  cbv3  1630  sbalyz  1875  dvelimdf  1892  dvelimor  1894  abbid  2154  nfcd  2173  ralrimi  2390  r19.32r  2457  ceqsalg  2582  ceqsex  2592  vtocldf  2605  elrab3t  2697  morex  2725  sbciedf  2798  csbiebt  2886  csbiedf  2887  ssrd  2950  rgenm  3323  invdisj  3759  ssopab2b  4013  eusv2nf  4188  sniota  4894  imadif  4979  funimaexglem  4982  eusvobj1  5499  ssoprab2b  5562  ovmpt2dxf  5626