Theorem 19.23aiv 1295

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

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  19.23aivv 1296  mo 1393  mopick 1433  zfext2 1461  gencl 1828  cgsexg 1831  gencbvex2 1839  vtocleg 1855  eqvinc 1883  uniiunlem 2132  eluni 2506  axsep2 2704  bm1.3ii 2706  intex 2729  unipw 2756  moabex 2766  nnullss 2768  exss 2769  mosubopt 2804  ssopab2 2822  reuunisn 2895  limuni3 3123  findsg 3157  tfindsg 3162  relop 3275  dmrnssfld 3357  elxp5 3454  unixp0 3518  ffoss 3711  fvopabn 3786  exfo 3822  tfrlem8 3918  tfrlem9 3919  fnoprabg 4012  erref 4275  ectocl 4302  ecoptocl 4303  mapprc 4326  map0b 4343  map0 4344  uniixp 4357  breng 4375  brdomg 4376  ener 4410  en0 4423  en1 4426  2dom 4427  undom 4438  xpdom2 4442  xpdom3 4445  pw2en 4446  mapen 4491  mapdom1 4492  mapdom2 4494  ssenen 4504  php 4513  0sdom1dom 4525  unfilem1 4548  unifiOLD 4557  fodomfiOLD 4566  pm54.43 4572  inf3 4620  infeq5 4621  omex 4627  zfregs 4647  tz9.12lem1 4659  bnd2 4724  aceq3lem 4732  aceq4 4734  aceq5lem4 4738  aceq5lem5 4739  aceq5 4740  aceq6a 4741  aceq6b 4742  ac6lem 4754  ac6s 4756  kmlem2 4766  kmlem16 4780  numthlem 4783  weth 4787  brdom3 4801  brdom5 4802  brdom4 4803  brdom7disj 4804  brdom6disj 4805  unidom 4808  oncard 4829  carduni 4858  cardcf 4911  cfeq0 4914  cfsuc 4915  cfom 4916  ltbtwnpq 5084  ltaprlem 5150  reclem1pr 5156  reclem2pr 5157  reclem3pr 5158  map2psrpr 5220  supsrlem2 5226  suprelem 5259  renegcl 5416  0re 5440  redivcl 5798  nnunb 6070  isumshft 7204  isumshft2 7205  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  infxpidmlem4 7555  infxpidmlem7 7558  infxpidmlem10 7561  infxpidmlem12 7563  infpss 7574  infmap2lem2 7580  tgval3t 7625  eltg3t 7626  bastop 7642  subbas2OLD 7645  isgrp2i 8076  minvecex 8578  projlem 9217  shintcl 9293  pjrn 9647  strlem1 10177  uninqs 10441  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  fiiu 10453  fiiuOLD 10454  ficli 10472  ficliOLD 10473  fiv 10482  fivOLD 10483  fiiu2 10488  fiiu2OLD 10489  homcard 10539  fisub 10576  fisubOLD 10577  infi 10578  infiOLD 10579  rcfpfillem2 10587  rcfpfillem2OLD 10588  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981

Copyright terms: Public domain