Theorem reximdva 2579

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  reximddv  2580  reximddv2  2582  dffo4  5664  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  prarloclemarch  7416  appdivnq  7561  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemloc  7605  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  archrecpr  7662  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemladdfu  7675  caucvgprlemlim  7679  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemexbt  7704  caucvgprprlemlim  7709  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemlub  7722  archsr  7780  suplocsrlemb  7804  suplocsrlempr  7805  cnegexlem2  8132  bndndx  9174  elpq  9647  qbtwnxr  10257  expnbnd  10643  expnlbnd2  10645  caucvgre  10989  cvg1nlemres  10993  r19.29uz  11000  resqrexlemglsq  11030  resqrexlemga  11031  cau3lem  11122  qdenre  11210  2clim  11308  climcn1  11315  climcn2  11316  climsqz  11342  climsqz2  11343  climcau  11354  divcnv  11504  divalglemex  11926  dvdsbnd  11956  bezoutlemzz  12002  bezoutlemaz  12003  bezoutlembz  12004  bezoutlembi  12005  lcmgcdlem  12076  divgcdcoprmex  12101  exprmfct  12137  prmdvdsfz  12138  pclemub  12286  pc2dvds  12328  pcprmpw  12332  dvdsprmpweqle  12335  infpnlem2  12357  prmunb  12359  ennnfonelemhom  12415  ctinf  12430  sgrpidmndm  12820  grpinveu  12910  dfgrp3mlem  12967  ringadd2  13208  cnpnei  13689  txlm  13749  metequiv2  13966  metrest  13976  mulc1cncf  14046  cncfco  14048  dedekindeulemlu  14069  suplociccreex  14072  dedekindicclemlu  14078  ivthinc  14091  cnplimcim  14106  cnplimclemr  14108  limccnpcntop  14114  limccoap  14117  subctctexmid  14720