Theorem 19.23aiv 1333

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 1007	. 2 |- (ps -> A.xps)
2		19.23aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.23ai 1100	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  E.wex 1016

This theorem is referenced by:  19.23aivv 1334  mo 1432  mopick 1472  axext3 1502  gencl 1874  cgsexg 1877  gencbvex2 1885  vtocleg 1901  eqvinc 1929  uniiunlem 2184  eluni 2572  axsep2 2778  bm1.3ii 2780  intex 2803  axpweq 2817  unipw 2836  moabex 2844  nnullss 2846  exss 2847  mosubopt 2881  ssopab2 2900  reuunisn 3118  limuni3 3206  tfindsg 3213  findsg 3245  relop 3365  dmrnssfld 3444  elxp5 3586  unixp0 3623  ffoss 3822  fvopabn 3897  exfo 3936  fnoprabg 4072  fo1stres 4156  fo2ndres 4157  tfrlem8 4219  tfrlem9 4220  erref 4415  mapprc 4467  map0b 4484  map0 4485  uniixp 4498  breng 4516  brdomg 4517  ener 4551  en0 4564  en1 4567  2dom 4568  fiprc 4574  undom 4579  xpdom2 4583  xpdom3 4586  pw2en 4587  ac6sfi 4591  mapen 4638  mapdom1 4639  mapdom2 4641  ssenen 4651  php 4660  0sdom1dom 4671  unfilem1 4694  unifi 4701  fodomfi 4709  pm54.43 4715  inf3 4765  infeq5 4766  omex 4772  zfregs 4793  tz9.12lem1 4805  bnd2 4870  aceq3lem 4878  aceq4 4880  aceq5lem4 4884  aceq5lem5 4885  aceq5 4886  aceq6a 4887  aceq6b 4888  ac6lem 4900  ac6s 4902  kmlem2 4912  kmlem16 4926  numthlem 4929  weth 4933  brdom3 4947  brdom5 4948  brdom4 4949  brdom7disj 4950  brdom6disj 4951  unidom 4954  oncard 4976  carduni 5008  cardcf 5061  cfeq0 5064  cfsuc 5065  cfom 5066  ltbtwnpq 5238  ltaprlem 5304  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  map2psrpr 5374  supsrlem2 5380  suprelem 5413  renegcli 5570  0re 5594  redivcli 5938  nnunb 6238  isumshfti 7408  isumshft2i 7409  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  infxpidmlem4 7767  infxpidmlem7 7770  infxpidmlem10 7773  infxpidmlem12 7775  infpss 7786  infmap2lem2 7792  tgval3 7837  eltg3 7838  bastop1 7854  subbas2 7857  isgrp2i 8293  minvecex 8838  grothpw 9054  projlem 9493  shintcli 9569  pjrni 9925  strlem1 10458  uninqs 10730  infi1 10735  fine 10736  fiiu 10738  ficli 10756  f1fi 10779  domleqt 10792  prj1 10809  fiv 10849  fiiu2 10852  infi 10854  inposet 10868  osneisi 11018  homcard 11045  fisub 11085  rcfpfillem2 11090  rcfpfillem3 11091  rcfpfillem4 11092  rcfpfillem6 11094  rcfpfil 11095  bwt2 11123  compsub 11488  hscptsscld 11491  compfipin0 11493  alexsublem2 11497  alexsub 11500  reconn 11512  isfne3 11543  topmtcl 11586  fbssint 11626  filrn 11643  fcluscomplem 11732  filnetlem1 11763  isga 11772  gapm 11784  morex 11804  oprabopabf 11807  fimax 11837  indexd 11846  heiborlem11 12021  heiborlem13 12023  heiborlem40 12050

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017

Copyright terms: Public domain