Theorem 19.23aiv 1337

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23aiv.1	|- (ph -> ps)

Assertion

Ref	Expression
19.23aiv	|- (E.xph -> ps)

Distinct variable group:   ps,x

Proof of Theorem 19.23aiv

Step	Hyp	Ref	Expression
1		ax-17 1012	. 2 |- (ps -> A.xps)
2		19.23aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.23ai 1105	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  E.wex 1021

This theorem is referenced by:  19.23aivv 1338  mo 1435  mopick 1475  axext3 1506  gencl 1875  cgsexg 1878  gencbvex2 1886  vtocleg 1902  eqvinc 1930  uniiunlem 2183  eluni 2560  axsep2 2759  bm1.3ii 2761  intex 2784  unipw 2812  moabex 2822  nnullss 2824  exss 2825  mosubopt 2860  ssopab2 2878  reuunisn 2952  limuni3 3180  findsg 3214  tfindsg 3219  relop 3332  dmrnssfld 3414  elxp5 3511  unixp0 3575  ffoss 3768  fvopabn 3843  exfo 3879  tfrlem8 3976  tfrlem9 3977  fnoprabg 4070  erref 4333  ectocl 4363  ecoptocl 4364  mapprc 4387  map0b 4404  map0 4405  uniixp 4418  breng 4436  brdomg 4437  ener 4471  en0 4484  en1 4487  2dom 4488  fiprc 4495  fiprOLD 4496  undom 4501  xpdom2 4505  xpdom3 4508  pw2en 4509  mapen 4556  mapdom1 4557  mapdom2 4559  ssenen 4569  php 4578  0sdom1dom 4589  unfilem1 4611  unifi 4618  fodomfi 4626  pm54.43 4632  inf3 4682  infeq5 4683  omex 4689  zfregs 4709  tz9.12lem1 4721  bnd2 4786  aceq3lem 4794  aceq4 4796  aceq5lem4 4800  aceq5lem5 4801  aceq5 4802  aceq6a 4803  aceq6b 4804  ac6lem 4816  ac6s 4818  kmlem2 4828  kmlem16 4842  numthlem 4845  weth 4849  brdom3 4863  brdom5 4864  brdom4 4865  brdom7disj 4866  brdom6disj 4867  unidom 4870  oncard 4892  carduni 4923  cardcf 4976  cfeq0 4979  cfsuc 4980  cfom 4981  ltbtwnpq 5149  ltaprlem 5215  reclem1pr 5221  reclem2pr 5222  reclem3pr 5223  map2psrpr 5285  supsrlem2 5291  suprelem 5324  renegcli 5481  0re 5505  redivcli 5856  nnunb 6152  isumshfti 7294  isumshft2i 7295  acdc3 7579  acdc2 7582  acdc5 7585  acdc 7587  infxpidmlem4 7647  infxpidmlem7 7650  infxpidmlem10 7653  infxpidmlem12 7655  infpss 7666  infmap2lem2 7672  tgval3 7714  eltg3 7715  bastop1 7731  isgrp2i 8160  minvecex 8662  projlem 9300  shintcli 9376  pjrni 9730  strlem1 10261  uninqs 10527  infi1 10532  fine 10533  fiiu 10535  ficli 10553  fiv 10571  fiiu2 10574  inposet 10578  homcard 10633  fisub 10666  infi 10667  rcfpfillem2 10672  rcfpfillem3 10673  rcfpfillem4 10674  rcfpfillem6 10676  rcfpfil 10677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022

Copyright terms: Public domain