Theorem reximdva 2579

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

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

Assertion

Ref	Expression
reximdva	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 115	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2577	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   E.wrex 2456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  reximddv  2580  reximddv2  2582  dffo4  5667  ctm  7111  ctssdclemn0  7112  ctssdccl  7113  ctssdc  7115  prarloclemarch  7420  appdivnq  7565  ltexprlemm  7602  ltexprlemopl  7603  ltexprlemopu  7605  ltexprlemloc  7609  archpr  7645  cauappcvgprlemm  7647  cauappcvgprlemopl  7648  cauappcvgprlemlol  7649  cauappcvgprlemopu  7650  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  archrecpr  7666  caucvgprlemm  7670  caucvgprlemopl  7671  caucvgprlemlol  7672  caucvgprlemopu  7673  caucvgprlemladdfu  7679  caucvgprlemlim  7683  caucvgprprlemml  7696  caucvgprprlemopl  7699  caucvgprprlemlol  7700  caucvgprprlemopu  7701  caucvgprprlemexbt  7708  caucvgprprlemlim  7713  suplocexprlemmu  7720  suplocexprlemru  7721  suplocexprlemlub  7726  archsr  7784  suplocsrlemb  7808  suplocsrlempr  7809  cnegexlem2  8136  bndndx  9178  elpq  9651  qbtwnxr  10261  expnbnd  10647  expnlbnd2  10649  caucvgre  10993  cvg1nlemres  10997  r19.29uz  11004  resqrexlemglsq  11034  resqrexlemga  11035  cau3lem  11126  qdenre  11214  2clim  11312  climcn1  11319  climcn2  11320  climsqz  11346  climsqz2  11347  climcau  11358  divcnv  11508  divalglemex  11930  dvdsbnd  11960  bezoutlemzz  12006  bezoutlemaz  12007  bezoutlembz  12008  bezoutlembi  12009  lcmgcdlem  12080  divgcdcoprmex  12105  exprmfct  12141  prmdvdsfz  12142  pclemub  12290  pc2dvds  12332  pcprmpw  12336  dvdsprmpweqle  12339  infpnlem2  12361  prmunb  12363  ennnfonelemhom  12419  ctinf  12434  sgrpidmndm  12827  grpinveu  12917  dfgrp3mlem  12974  ringadd2  13216  cnpnei  13859  txlm  13919  metequiv2  14136  metrest  14146  mulc1cncf  14216  cncfco  14218  dedekindeulemlu  14239  suplociccreex  14242  dedekindicclemlu  14248  ivthinc  14261  cnplimcim  14276  cnplimclemr  14278  limccnpcntop  14284  limccoap  14287  subctctexmid  14891