Theorem r19.23adva 1723

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

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 1105  E.wrex 1622

This theorem is referenced by:  r19.23aivv 1724  r19.23advv 1725  elunirnALT 3808  oawordexr 4128  oarec 4134  odi 4148  nneob 4193  onfin 4451  isfinite2 4475  cnegextlem1 5268  cnegextlem2 5269  cnegextlem3 5270  1re 5358  0re 5363  ioo0t 6256  sqr2irr 6610  seq1bnd 6798  infxpidmlem7 7452  infxpidmlem8 7453  infxpidmlem10 7455  tgclt 7517  subtop 7539  retopbas 7548  neindisj 7620  innei 7625  blssex 7742  metcnp 7774  lmle 7843  iscms2lem4 7874  bcthlem13 7893  ghgrpilem2 8019  nmobndi 8305  ubthlem5 8399  omlsi 9374  shsel3t 9408  spansncol 9621  nmopunt 10068  riesz1t 10127  hmopidmch 10204  cvcon3t 10335  chcv1t 10404  atcvatlem 10434  irred 10443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-17 1190

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-rex 1626

Copyright terms: Public domain