Theorem alrimi 1575

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

This proof depends on syntax axioms:   -> wi 4   A.wal 1400   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  axc4i  1595  19.32r  1732  cbv3  1795  sbbid  1899  sbalyz  2059  dvelimdf  2076  dvelimor  2078  nf5d  2085  abbid  2355  nfcd  2387  nfabdw  2411  ralrimi  2621  r19.32r  2697  ceqsalg  2850  ceqsex  2860  vtocldf  2874  elrab3t  2981  morex  3010  sbciedf  3087  csbiebt  3187  csbiedf  3188  ssrd  3253  invdisj  4123  ssopab2b  4421  eusv2nf  4604  sniota  5371  imadif  5464  funimaexglem  5467  eusvobj1  6075  ssoprab2b  6148  ovmpodxf  6217  modom  7112  nninfinf  10901