Theorem r19.23adva 2216

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 402	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	r19.23adv 2215	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  r19.23aivv 2217  r19.23advv 2218  elunirnALT 4845  oawordexr 5238  oarec 5244  odi 5258  nneob 5312  onfin 5613  isfinite2 5639  cnegexlem1 6499  cnegexlem2 6500  cnegexlem3 6501  1re 6598  0re 6603  ioo0 7535  sqr2irr 7979  seq1bndi 8162  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem10 8830  tgcl 8894  subtop 8916  retopbas 8925  neindisj 9007  innei 9012  blssex 9131  metcnp 9165  lmle 9238  iscms2lem4 9270  bcthlem13 9289  ghgrpilem2 9442  nmobndi 9777  ubthlem5 9876  dif1en 10172  indexfi 10174  fipreima 10175  ficard 10176  dif1card 10177  subspid 10249  subcld 10254  omlsii 10878  shsel3 10912  spansncol 11124  nmopun 11576  riesz1 11635  hmopidmchi 11723  cvcon3 11856  chcv1 11927  atcvatlem 11957  irredi 11966  axfelem16 14046  opncldf1 15402  opnregcld 15415  cldregopn 15416  subsubtop 15423  compsub 15431  flimcls 15588  rnelfm 15593  fmfnfm 15598  fcluscomp 15621  tailmap 15636  filnetlem5 15644  foco2 15686  cocanfo 15689  f1elima 15719  indexfiOLD 15755  fipreimaOLD 15756  frfi 15771  filbcmb 15776  fdc 15812  fdc1 15813  incsequz 15815  subspcld2 15839  subspabs 15840  caushft 15851  cnimass 15888  cnresima 15891  txsubsp 15912  sstotbnd 15936  totbndss 15937  totbndbnd 15944  ismtyhmeolem 15950  heiborlem1 15955  heiborlem11 15965  heiborlem13 15967  heiborlem15 15969  heiborlem16 15970  heiborlem23 15977  heiborlem28 15982  heiborlem35 15989  pi1gp 16095  divrngidl 16176  prnc 16215  cvrcon3b 16994  atomnle 17016  hlhght2 17038  hl0lt1 17039  hl2atom 17053  cvrexchlem 17059  cvratlem 17061  ispsubcl2 17356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain