Theorem alrimi 1412

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1	|- F/xph
alrimi.2	|- (ph -> ps)

Assertion

Ref	Expression
alrimi	|- (ph -> A.xps)

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3 |- F/xph
2	1	nfri 1409	. 2 |- (ph -> A.xph)
3		alrimi.2	. 2 |- (ph -> ps)
4	2, 3	alrimih 1355	1 |- (ph -> A.xps)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1333  ax-gen 1335  ax-4 1397

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

This theorem is referenced by:  19.32r  1567  cbv3  1627  sbalyz  1872  dvelimdf  1889  dvelimor  1891  abbid  2151  nfcd  2170  ralrimi  2384  r19.32r  2451  ceqsalg  2576  ceqsex  2586  vtocldf  2599  elrab3t  2691  morex  2719  sbciedf  2792  csbiebt  2880  csbiedf  2881  ssrd  2944  rgenm  3317  invdisj  3750  ssopab2b  4004  eusv2nf  4154  sniota  4837  imadif  4922  funimaexglem  4925  eusvobj1  5442  ssoprab2b  5504  ovmpt2dxf  5568