Theorem r19.23adva 1793

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).

Hypothesis

Ref	Expression
r19.23adva.1	|- ((ph /\ x e. A) -> (ps -> ch))

Assertion

Ref	Expression
r19.23adva	|- (ph -> (E.x e. A ps -> ch))

Distinct variable groups:   ph,x   ch,x

Proof of Theorem r19.23adva

Step	Hyp	Ref	Expression
1		r19.23adva.1	. . 3 |- ((ph /\ x e. A) -> (ps -> ch))
2	1	ex 371	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	r19.23adv 1792	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 994  E.wrex 1692

This theorem is referenced by:  r19.23aivv 1794  r19.23advv 1795  elunirnALT 3983  oawordexr 4326  oarec 4332  odi 4346  nneob 4395  onfin 4666  isfinite2 4692  cnegexlem1 5499  cnegexlem2 5500  cnegexlem3 5501  1re 5589  0re 5594  ioo0 6494  sqr2irr 6930  seq1bndi 7113  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem10 7773  tgcl 7836  subtop 7858  retopbas 7865  neindisj 7941  innei 7946  blssex 8064  metcnp 8098  lmle 8171  iscms2lem4 8203  bcthlem13 8222  ghgrpilem2 8375  nmobndi 8692  ubthlem5 8791  omlsii 9521  shsel3 9555  spansncol 9767  nmopun 10218  riesz1 10277  hmopidmchi 10359  cvcon3 10492  chcv1 10563  atcvatlem 10594  irredi 10603  opncldf1 11454  opnregcld 11467  cldregopn 11468  subspid 11478  subsubtop 11479  subcld 11480  compsub 11488  flimcls 11684  rnelfm 11699  fmfnfm 11704  fcluscomp 11733  tailmap 11759  filnetlem5 11767  f1elima 11818  ficard 11834  dif1card 11835  indexf 11847  fipreima 11848  filbcmb 11857  incsequz 11879  subspcld2 11902  subspabs 11903  metsstop 11909  caushft 11916  cnimass 11949  cnresima 11952  txsubsp 11983  sstotbnd 11992  totbndss 11993  totbndbnd 12000  ismtyhmeolem 12006  heiborlem1 12011  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem16 12026  heiborlem23 12033  heiborlem28 12038  heiborlem35 12045

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  df-rex 1696

Copyright terms: Public domain