Theorem reximdva 2572

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

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  reximddv  2573  reximddv2  2575  dffo4  5644  ctm  7086  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  prarloclemarch  7380  appdivnq  7525  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  archrecpr  7626  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemladdfu  7639  caucvgprlemlim  7643  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemexbt  7668  caucvgprprlemlim  7673  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemlub  7686  archsr  7744  suplocsrlemb  7768  suplocsrlempr  7769  cnegexlem2  8095  bndndx  9134  elpq  9607  qbtwnxr  10214  expnbnd  10599  expnlbnd2  10601  caucvgre  10945  cvg1nlemres  10949  r19.29uz  10956  resqrexlemglsq  10986  resqrexlemga  10987  cau3lem  11078  qdenre  11166  2clim  11264  climcn1  11271  climcn2  11272  climsqz  11298  climsqz2  11299  climcau  11310  divcnv  11460  divalglemex  11881  dvdsbnd  11911  bezoutlemzz  11957  bezoutlemaz  11958  bezoutlembz  11959  bezoutlembi  11960  lcmgcdlem  12031  divgcdcoprmex  12056  exprmfct  12092  prmdvdsfz  12093  pclemub  12241  pc2dvds  12283  pcprmpw  12287  dvdsprmpweqle  12290  infpnlem2  12312  prmunb  12314  ennnfonelemhom  12370  ctinf  12385  sgrpidmndm  12656  grpinveu  12741  cnpnei  13013  txlm  13073  metequiv2  13290  metrest  13300  mulc1cncf  13370  cncfco  13372  dedekindeulemlu  13393  suplociccreex  13396  dedekindicclemlu  13402  ivthinc  13415  cnplimcim  13430  cnplimclemr  13432  limccnpcntop  13438  limccoap  13441  subctctexmid  14034