Theorem reximdva 2567

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

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2448  df-rex 2449

This theorem is referenced by:  reximddv  2568  reximddv2  2570  dffo4  5632  ctm  7070  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  prarloclemarch  7355  appdivnq  7500  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  archpr  7580  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  archrecpr  7601  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemladdfu  7614  caucvgprlemlim  7618  caucvgprprlemml  7631  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemexbt  7643  caucvgprprlemlim  7648  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemlub  7661  archsr  7719  suplocsrlemb  7743  suplocsrlempr  7744  cnegexlem2  8070  bndndx  9109  elpq  9582  qbtwnxr  10189  expnbnd  10574  expnlbnd2  10576  caucvgre  10919  cvg1nlemres  10923  r19.29uz  10930  resqrexlemglsq  10960  resqrexlemga  10961  cau3lem  11052  qdenre  11140  2clim  11238  climcn1  11245  climcn2  11246  climsqz  11272  climsqz2  11273  climcau  11284  divcnv  11434  divalglemex  11855  dvdsbnd  11885  bezoutlemzz  11931  bezoutlemaz  11932  bezoutlembz  11933  bezoutlembi  11934  lcmgcdlem  12005  divgcdcoprmex  12030  exprmfct  12066  prmdvdsfz  12067  pclemub  12215  pc2dvds  12257  pcprmpw  12261  dvdsprmpweqle  12264  infpnlem2  12286  prmunb  12288  ennnfonelemhom  12344  ctinf  12359  cnpnei  12819  txlm  12879  metequiv2  13096  metrest  13106  mulc1cncf  13176  cncfco  13178  dedekindeulemlu  13199  suplociccreex  13202  dedekindicclemlu  13208  ivthinc  13221  cnplimcim  13236  cnplimclemr  13238  limccnpcntop  13244  limccoap  13247  subctctexmid  13841