Theorem reximdva 2632

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  reximddv  2633  reximddv2  2635  dffo4  5783  ctm  7276  ctssdclemn0  7277  ctssdccl  7278  ctssdc  7280  prarloclemarch  7605  appdivnq  7750  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemloc  7794  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemopu  7835  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  archrecpr  7851  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemopu  7858  caucvgprlemladdfu  7864  caucvgprlemlim  7868  caucvgprprlemml  7881  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemexbt  7893  caucvgprprlemlim  7898  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemlub  7911  archsr  7969  suplocsrlemb  7993  suplocsrlempr  7994  cnegexlem2  8322  bndndx  9368  elpq  9844  qbtwnxr  10477  expnbnd  10885  expnlbnd2  10887  caucvgre  11492  cvg1nlemres  11496  r19.29uz  11503  resqrexlemglsq  11533  resqrexlemga  11534  cau3lem  11625  qdenre  11713  2clim  11812  climcn1  11819  climcn2  11820  climsqz  11846  climsqz2  11847  climcau  11858  divcnv  12008  divalglemex  12433  dvdsbnd  12477  bezoutlemzz  12523  bezoutlemaz  12524  bezoutlembz  12525  bezoutlembi  12526  lcmgcdlem  12599  divgcdcoprmex  12624  exprmfct  12660  prmdvdsfz  12661  pclemub  12810  pc2dvds  12853  pcprmpw  12857  dvdsprmpweqle  12860  infpnlem2  12883  prmunb  12885  ennnfonelemhom  12986  ctinf  13001  sgrpidmndm  13453  grpinveu  13571  dfgrp3mlem  13631  ringadd2  13990  znunit  14623  cnpnei  14893  txlm  14953  metequiv2  15170  metrest  15180  mulc1cncf  15263  cncfco  15265  dedekindeulemlu  15295  suplociccreex  15298  dedekindicclemlu  15304  ivthinc  15317  cnplimcim  15341  cnplimclemr  15343  limccnpcntop  15349  limccoap  15352  elply2  15409  subctctexmid  16366