Theorem reximdv2 2934

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 1686	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2820	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2820	. 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 1596   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-rex 2820

This theorem is referenced by:  ssrexv  3565  ssimaex  5930  nnsuc  6695  oaass  7207  omeulem1  7228  ssnnfi  7736  findcard3  7759  unfilem1  7780  epfrs  8158  alephval3  8487  isfin7-2  8772  fin1a2lem6  8781  fpwwe2lem12  9015  fpwwe2lem13  9016  inawinalem  9063  ico0  11571  ioc0  11572  r19.2uz  13143  climrlim2  13329  iserodd  14214  ramub2  14387  pgpssslw  16430  efgrelexlemb  16564  ablfaclem3  16928  unitgrp  17100  lspsneq  17551  lbsextlem4  17590  neissex  19394  iscnp4  19530  nlly2i  19743  llynlly  19744  restnlly  19749  llyrest  19752  nllyrest  19753  llyidm  19755  nllyidm  19756  qtophmeo  20053  cnpflfi  20235  cnextcn  20302  ivthlem3  21600  ovolicc2lem5  21667  dvfsumrlim  22167  itgsubst  22185  lgsquadlem2  23358  footex  23803  nbgraf1olem5  24121  cusgrafilem2  24156  eulerpartlemgvv  27955  eulerpartlemgh  27957  erdszelem7  28281  rellyscon  28336  trpredrec  28898  itg2gt0cn  29647  ivthALT  29730  fnessref  29765  frinfm  29829  sstotbnd2  29873  heiborlem3  29912  isdrngo3  29965  pellexlem5  30373  pell14qrss1234  30396  pell1qrss14  30408  pellfundglb  30425  lnr2i  30669  hbtlem6  30682  dihjat1lem  36225  dvh1dim  36239  dochsatshp  36248  lcfl6  36297  mapdval2N  36427  mapdpglem2  36470  hdmaprnlem10N  36659