Theorem alrimi 1765

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 1762	. 2 |- (ph -> A.xph)
3		alrimi.2	. 2 |- (ph -> ps)
4	2, 3	alrimih 1565	1 |- (ph -> A.xps)

Syntax hints:   -> wi 4  A.wal 1540   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  nfd  1766  a5i  1789  exlimd  1806  19.12  1847  nfald  1852  nfaldOLD  1853  19.38OLD  1874  equs5e  1888  equsal  1960  sbbid  2078  dvelimdf  2082  sb6rf  2091  sb8  2092  nfsbd  2111  eupicka  2268  2moex  2275  abbid  2467  nfcd  2485  ralrimi  2696  ceqsalg  2884  ceqsex  2894  vtocldf  2907  morex  3021  sbciedf  3082  csbiebt  3173  csbiedf  3174  iota2df  4366  sniota  4370  ncfinlower  4484  ssopab2b  4714  imadif  5172