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  10066  qbtwnxr  10709  expnbnd  11122  expnlbnd2  11124  caucvgre  11769  cvg1nlemres  11773  r19.29uz  11780  resqrexlemglsq  11810  resqrexlemga  11811  cau3lem  11903  qdenre  11991  2clim  12092  climcn1  12099  climcn2  12100  climsqz  12126  climsqz2  12127  climcau  12138  divcnv  12289  divalglemex  12714  dvdsbnd  12758  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlembi  12807  lcmgcdlem  12880  divgcdcoprmex  12905  exprmfct  12942  prmdvdsfz  12943  pclemub  13095  pc2dvds  13138  pcprmpw  13142  dvdsprmpweqle  13145  infpnlem2  13168  prmunb  13170  ennnfonelemhom  13364  ctinf  13379  sgrpidmndm  13792  grpinveu  13902  dfgrp3mlem  13962  ringadd2  14439  znunit  15103  cnpnei  15445  txlm  15505  metequiv2  15722  metrest  15732  mulc1cncf  15815  cncfco  15817  dedekindeulemlu  15847  suplociccreex  15850  dedekindicclemlu  15856  ivthinc  15869  cnplimcim  15893  cnplimclemr  15895  limccnpcntop  15901  limccoap  15904  elply2  15961  clwwlkn1loopb  16866  subctctexmid  17235