Theorem alrimiv 1631

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
alrimiv.1	|- (ph -> ps)

Assertion

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

Distinct variable group:   ph,x

Allowed substitution hint:   ps(x)

Proof of Theorem alrimiv

Step	Hyp	Ref	Expression
1		ax-17 1616	. 2 |- (ph -> A.xph)
2		alrimiv.1	. 2 |- (ph -> ps)
3	1, 2	alrimih 1565	1 |- (ph -> A.xps)

Syntax hints:   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem is referenced by:  alrimivv  1632  nfdv  1639  cbvalivw  1674  spOLD  1748  ax9  1949  cbvald  2008  ax10-16  2190  ax11eq  2193  ax11el  2194  axext4  2337  eqrdv  2351  abbi2dv  2468  abbi1dv  2469  elex22  2870  elex2  2871  spcimdv  2936  pm13.183  2979  moeq3  3013  sbc2or  3054  sbcthdv  3061  sbcimdv  3107  ssrdv  3278  ss2abdv  3339  abssdv  3340  dfnfc2  3909  intss  3947  intab  3956  dfiin2g  4000  setswith  4321  iotaval  4350  iota5  4359  iotabidv  4360  sfintfin  4532  vfinspss  4551  vfinspclt  4552  phidisjnn  4615  eqoprrdv  4854  funco  5142  funun  5146  fununi  5160  funcnvuni  5161  nfunsn  5353  funsi  5520  funoprabg  5583  mpteq12dv  5656  fntxp  5804  fnpprod  5843  clos1is  5881  fundmen  6043  enpw1  6062  enmap2lem4  6066  enmap1lem4  6072  enprmaplem3  6078  ncprc  6124  fnfrec  6320