Theorem reximdv2 2858

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 1764	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2743	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2743	. 2 |- ( E. x e. B ch <-> E. x ( x e. B /\ ch ) )
5	2, 3, 4	3imtr4g 274	1 |- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )

Syntax hints:   -> wi 4   /\ wa 371   E.wex 1663   e. wcel 1887   E.wrex 2738

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

This theorem depends on definitions:  df-bi 189  df-ex 1664  df-rex 2743

This theorem is referenced by:  ssrexv  3494  ssimaex  5930  nnsuc  6709  oaass  7262  omeulem1  7283  ssnnfi  7791  findcard3  7814  unfilem1  7835  epfrs  8215  alephval3  8541  isfin7-2  8826  fin1a2lem6  8835  fpwwe2lem12  9066  fpwwe2lem13  9067  inawinalem  9114  ico0  11682  ioc0  11683  r19.2uz  13414  climrlim2  13611  iserodd  14785  ramub2  14971  prmgaplem6  15026  pgpssslw  17266  efgrelexlemb  17400  ablfaclem3  17720  unitgrp  17895  lspsneq  18345  lbsextlem4  18384  neissex  20143  iscnp4  20279  nlly2i  20491  llynlly  20492  restnlly  20497  llyrest  20500  nllyrest  20501  llyidm  20503  nllyidm  20504  qtophmeo  20832  cnpflfi  21014  cnextcn  21082  ivthlem3  22404  ovolicc2lem5  22475  dvfsumrlim  22983  itgsubst  23001  lgsquadlem2  24283  footex  24763  opphllem1  24789  oppperpex  24795  outpasch  24797  nbgraf1olem5  25173  cusgrafilem2  25208  cmppcmp  28685  eulerpartlemgvv  29209  eulerpartlemgh  29211  erdszelem7  29920  rellyscon  29974  trpredrec  30479  ivthALT  30991  fnessref  31013  phpreu  31929  poimirlem26  31966  itg2gt0cn  31997  frinfm  32062  sstotbnd2  32106  heiborlem3  32145  isdrngo3  32198  dihjat1lem  34996  dvh1dim  35010  dochsatshp  35019  lcfl6  35068  mapdval2N  35198  mapdpglem2  35241  hdmaprnlem10N  35430  pellexlem5  35677  pell14qrss1234  35702  pell1qrss14  35714  pellfundglb  35733  lnr2i  35975  hbtlem6  35988  ushgredgedga  39306  ushgredgedgaloop  39308  cusgrfilem2  39517