Theorem r19.23adv 1286

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

Hypothesis

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

Assertion

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

Distinct variable group(s):   ph,x   ch,x

Proof of Theorem r19.23adv

Step	Hyp	Ref	Expression
1		r19.23adv.1	. . . 4 |- (ph -> (x e. A -> (ps -> ch)))
2	1	imp3a 279	. . 3 |- (ph -> ((x e. A /\ ps) -> ch))
3	2	19.23adv 954	. 2 |- (ph -> (E.x(x e. A /\ ps) -> ch))
4		df-rex 1206	. 2 |- (E.x e. A ps <-> E.x(x e. A /\ ps))
5	3, 4	syl5ib 181	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 2   /\ wa 196  E.wex 678   e. wcel 1092  E.wrex 1202

This theorem is referenced by:  r19.23aivv 1287  r19.23advv 1288  tz7.7 2224  ssorduni 2249  onint 2261  funcnvuni 2706  isofrlem 2939  tfrlem8 2956  tfrlem9 2957  oawordexr 3158  oaordex 3160  oalimcl 3162  oaass 3163  onfin 3415  finsucdom 3421  unblem1 3431  isfinite2 3437  inf3lem3 3466  tz9.12lem3 3505  karden 3551  aceq5lem4 3561  aceq5 3563  cardaleph 3690  cardinfima 3696  nndiv 4453  btwnz 4613  uzwo3lem1 4614  qbtwnre 4650  sqr2irr 4782  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  projlem13 5205  omlsi 5250  spansncol 5473  spansneleq 5475  spansnsst 5476  spanunsn 5482  h1datom 5483  cvcon3t 5716  chcv1t 5751  atcvatlem 5770

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-rex 1206

metamath.org