Theorem reximdv2 2929

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 1677	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2804	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2804	. 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 1587   e. wcel 1758   E.wrex 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-rex 2804

This theorem is referenced by:  ssrexv  3524  ssimaex  5864  nnsuc  6602  oaass  7109  omeulem1  7130  ssnnfi  7642  findcard3  7665  unfilem1  7686  epfrs  8061  alephval3  8390  isfin7-2  8675  fin1a2lem6  8684  fpwwe2lem12  8918  fpwwe2lem13  8919  inawinalem  8966  ico0  11456  ioc0  11457  r19.2uz  12956  climrlim2  13142  iserodd  14019  ramub2  14192  pgpssslw  16233  efgrelexlemb  16367  ablfaclem3  16709  unitgrp  16881  lspsneq  17325  lbsextlem4  17364  neissex  18862  iscnp4  18998  nlly2i  19211  llynlly  19212  restnlly  19217  llyrest  19220  nllyrest  19221  llyidm  19223  nllyidm  19224  qtophmeo  19521  cnpflfi  19703  cnextcn  19770  ivthlem3  21068  ovolicc2lem5  21135  dvfsumrlim  21635  itgsubst  21653  lgsquadlem2  22826  footex  23253  nbgraf1olem5  23505  cusgrafilem2  23539  eulerpartlemgvv  26902  eulerpartlemgh  26904  erdszelem7  27228  rellyscon  27283  trpredrec  27845  itg2gt0cn  28594  ivthALT  28677  fnessref  28712  frinfm  28776  sstotbnd2  28820  heiborlem3  28859  isdrngo3  28912  pellexlem5  29321  pell14qrss1234  29344  pell1qrss14  29356  pellfundglb  29373  lnr2i  29619  hbtlem6  29632  dihjat1lem  35396  dvh1dim  35410  dochsatshp  35419  lcfl6  35468  mapdval2N  35598  mapdpglem2  35641  hdmaprnlem10N  35830