Theorem reximdva 2532

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 114	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2530	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   E.wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420

This theorem is referenced by:  reximddv  2533  reximddv2  2535  dffo4  5561  ctm  6987  ctssdclemn0  6988  ctssdccl  6989  ctssdc  6991  prarloclemarch  7219  appdivnq  7364  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemloc  7408  archpr  7444  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  archrecpr  7465  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemladdfu  7478  caucvgprlemlim  7482  caucvgprprlemml  7495  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemopu  7500  caucvgprprlemexbt  7507  caucvgprprlemlim  7512  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemlub  7525  archsr  7583  suplocsrlemb  7607  suplocsrlempr  7608  cnegexlem2  7931  bndndx  8969  qbtwnxr  10028  expnbnd  10408  expnlbnd2  10410  caucvgre  10746  cvg1nlemres  10750  r19.29uz  10757  resqrexlemglsq  10787  resqrexlemga  10788  cau3lem  10879  qdenre  10967  2clim  11063  climcn1  11070  climcn2  11071  climsqz  11097  climsqz2  11098  climcau  11109  divcnv  11259  divalglemex  11608  dvdsbnd  11634  bezoutlemzz  11679  bezoutlemaz  11680  bezoutlembz  11681  bezoutlembi  11682  lcmgcdlem  11747  divgcdcoprmex  11772  exprmfct  11807  prmdvdsfz  11808  ennnfonelemhom  11917  ctinf  11932  cnpnei  12377  txlm  12437  metequiv2  12654  metrest  12664  mulc1cncf  12734  cncfco  12736  dedekindeulemlu  12757  suplociccreex  12760  dedekindicclemlu  12766  ivthinc  12779  cnplimcim  12794  cnplimclemr  12796  limccnpcntop  12802  limccoap  12805  subctctexmid  13185