Theorem r19.23adva 1744

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 1743	1 |- (ph -> (E.x e. A ps -> ch))

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

This theorem is referenced by:  r19.23aivv 1745  r19.23advv 1746  elunirnALT 3860  oawordexr 4180  oarec 4186  odi 4200  nneob 4245  onfin 4505  isfinite2 4529  cnegextlem1 5325  cnegextlem2 5326  cnegextlem3 5327  1re 5415  0re 5420  ioo0t 6313  sqr2irr 6667  seq1bnd 6855  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem10 7512  tgclt 7574  subtop 7596  retopbas 7605  neindisj 7681  innei 7686  blssex 7806  metcnp 7839  lmle 7911  iscms2lem4 7942  bcthlem13 7961  ghgrpilem2 8086  nmobndi 8383  ubthlem5 8477  omlsi 9183  shsel3t 9217  spansncol 9430  nmopunt 9877  riesz1t 9936  hmopidmch 10017  cvcon3t 10149  chcv1t 10219  atcvatlem 10249  irred 10258

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain