Theorem reximdv2 2815

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)

Hypothesis

Ref	Expression
reximdv2.1	|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )

Assertion

Ref	Expression
reximdv2	|- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem reximdv2

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 |- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )
2	1	eximdv 1675	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2711	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2711	. 2 |- ( E. x e. B ch <-> E. x ( x e. B /\ ch ) )
5	2, 3, 4	3imtr4g 270	1 |- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )

Syntax hints:   -> wi 4   /\ wa 369   E.wex 1589   e. wcel 1755   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-rex 2711

This theorem is referenced by:  ssrexv  3405  ssimaex  5744  nnsuc  6482  oaass  6988  omeulem1  7009  ssnnfi  7520  findcard3  7543  unfilem1  7564  epfrs  7939  alephval3  8268  isfin7-2  8553  fin1a2lem6  8562  fpwwe2lem12  8796  fpwwe2lem13  8797  inawinalem  8844  ico0  11334  ioc0  11335  r19.2uz  12823  climrlim2  13009  iserodd  13885  ramub2  14058  pgpssslw  16093  efgrelexlemb  16227  ablfaclem3  16562  unitgrp  16693  lspsneq  17125  lbsextlem4  17164  neissex  18573  iscnp4  18709  nlly2i  18922  llynlly  18923  restnlly  18928  llyrest  18931  nllyrest  18932  llyidm  18934  nllyidm  18935  qtophmeo  19232  cnpflfi  19414  cnextcn  19481  ivthlem3  20779  ovolicc2lem5  20846  dvfsumrlim  21345  itgsubst  21363  lgsquadlem2  22579  nbgraf1olem5  23177  cusgrafilem2  23211  eulerpartlemgvv  26607  eulerpartlemgh  26609  erdszelem7  26933  rellyscon  26988  trpredrec  27549  itg2gt0cn  28291  ivthALT  28374  fnessref  28409  frinfm  28473  sstotbnd2  28517  heiborlem3  28556  isdrngo3  28609  pellexlem5  29019  pell14qrss1234  29042  pell1qrss14  29054  pellfundglb  29071  lnr2i  29317  hbtlem6  29330  dihjat1lem  34646  dvh1dim  34660  dochsatshp  34669  lcfl6  34718  mapdval2N  34848  mapdpglem2  34891  hdmaprnlem10N  35080