Theorem alrimiv 1751

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 1416	. 2 |- (ph -> A.xph)
2		alrimiv.1	. 2 |- (ph -> ps)
3	1, 2	alrimih 1355	1 |- (ph -> A.xps)

Syntax hints:   -> wi 4  A.wal 1240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1333  ax-gen 1335  ax-17 1416

This theorem is referenced by:  alrimivv  1752  nfdv  1754  axext4  2021  eqrdv  2035  abbi2dv  2153  abbi1dv  2154  elex22  2563  elex2  2564  spcimdv  2631  spcimedv  2633  pm13.183  2675  sbcthdv  2772  sbcimdv  2817  ssrdv  2945  ss2abdv  3007  abssdv  3008  opprc  3561  dfnfc2  3589  intss  3627  intab  3635  dfiin2g  3681  disjss1  3742  mpteq12dva  3829  el  3922  euotd  3982  reusv1  4156  elirr  4224  sucprcreg  4227  en2lp  4232  tfisi  4253  ssrelrel  4383  issref  4650  iotaval  4821  iota5  4830  iotabidv  4831  funmo  4860  funco  4883  funun  4887  fununi  4910  funcnvuni  4911  funimaexglem  4925  fvssunirng  5133  relfvssunirn  5134  sefvex  5139  nfunsn  5150  f1oresrab  5272  funoprabg  5542  mpt2fvex  5771  1stconst  5784  2ndconst  5785  tfrexlem  5889  rdgexggg  5904  rdgifnon  5906  rdgifnon2  5907  rdgivallem  5908  frectfr  5924  frecrdg  5931  iserd  6068  pitonn  6744  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdgfn  8879  frecuzrdgsuc  8882  2spim  9241  bj-om  9396  bj-nnord  9418  bj-inf2vn  9434  bj-inf2vn2  9435  bj-findis  9439