Theorem reximdva 2652

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  reximddv  2653  reximddv2  2655  dffo4  5859  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  prarloclemarch  7791  appdivnq  7936  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  archrecpr  8037  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemladdfu  8050  caucvgprlemlim  8054  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  caucvgprprlemlim  8084  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemlub  8097  archsr  8155  suplocsrlemb  8179  suplocsrlempr  8180  cnegexlem2  8509  bndndx  9573  elpq  10065  qbtwnxr  10708  expnbnd  11121  expnlbnd2  11123  caucvgre  11768  cvg1nlemres  11772  r19.29uz  11779  resqrexlemglsq  11809  resqrexlemga  11810  cau3lem  11902  qdenre  11990  2clim  12091  climcn1  12098  climcn2  12099  climsqz  12125  climsqz2  12126  climcau  12137  divcnv  12288  divalglemex  12713  dvdsbnd  12757  bezoutlemzz  12803  bezoutlemaz  12804  bezoutlembz  12805  bezoutlembi  12806  lcmgcdlem  12879  divgcdcoprmex  12904  exprmfct  12941  prmdvdsfz  12942  pclemub  13094  pc2dvds  13137  pcprmpw  13141  dvdsprmpweqle  13144  infpnlem2  13167  prmunb  13169  ennnfonelemhom  13363  ctinf  13378  sgrpidmndm  13791  grpinveu  13901  dfgrp3mlem  13961  ringadd2  14438  znunit  15102  cnpnei  15462  txlm  15522  metequiv2  15739  metrest  15749  mulc1cncf  15832  cncfco  15834  dedekindeulemlu  15864  suplociccreex  15867  dedekindicclemlu  15873  ivthinc  15886  cnplimcim  15910  cnplimclemr  15912  limccnpcntop  15918  limccoap  15921  elply2  15978  clwwlkn1loopb  16883  subctctexmid  17252