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  2469  abbi1dv  2470  elex22  2871  elex2  2872  spcimdv  2937  pm13.183  2980  moeq3  3014  sbc2or  3055  sbcthdv  3062  sbcimdv  3108  ssrdv  3279  ss2abdv  3340  abssdv  3341  dfnfc2  3910  intss  3948  intab  3957  dfiin2g  4001  setswith  4322  iotaval  4351  iota5  4360  iotabidv  4361  sfintfin  4533  vfinspss  4552  vfinspclt  4553  phidisjnn  4616  eqoprrdv  4855  funco  5143  funun  5147  fununi  5161  funcnvuni  5162  nfunsn  5354  funsi  5521  funoprabg  5584  mpteq12dv  5657  fntxp  5805  fnpprod  5844  clos1is  5882  fundmen  6044  enpw1  6063  enmap2lem4  6067  enmap1lem4  6073  enprmaplem3  6079  ncprc  6125  fnfrec  6321