Theorem reximdva 2537

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  reximddv  2538  reximddv2  2540  dffo4  5576  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  prarloclemarch  7250  appdivnq  7395  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  archrecpr  7496  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemladdfu  7509  caucvgprlemlim  7513  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemexbt  7538  caucvgprprlemlim  7543  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemlub  7556  archsr  7614  suplocsrlemb  7638  suplocsrlempr  7639  cnegexlem2  7962  bndndx  9000  elpq  9467  qbtwnxr  10066  expnbnd  10446  expnlbnd2  10448  caucvgre  10785  cvg1nlemres  10789  r19.29uz  10796  resqrexlemglsq  10826  resqrexlemga  10827  cau3lem  10918  qdenre  11006  2clim  11102  climcn1  11109  climcn2  11110  climsqz  11136  climsqz2  11137  climcau  11148  divcnv  11298  divalglemex  11655  dvdsbnd  11681  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlembi  11729  lcmgcdlem  11794  divgcdcoprmex  11819  exprmfct  11854  prmdvdsfz  11855  ennnfonelemhom  11964  ctinf  11979  cnpnei  12427  txlm  12487  metequiv2  12704  metrest  12714  mulc1cncf  12784  cncfco  12786  dedekindeulemlu  12807  suplociccreex  12810  dedekindicclemlu  12816  ivthinc  12829  cnplimcim  12844  cnplimclemr  12846  limccnpcntop  12852  limccoap  12855  subctctexmid  13369