Theorem reximdv2 2894

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

Syntax hints:   -> wi 4   /\ wa 370   E.wex 1659   e. wcel 1867   E.wrex 2774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-rex 2779

This theorem is referenced by:  ssrexv  3523  ssimaex  5937  nnsuc  6714  oaass  7261  omeulem1  7282  ssnnfi  7788  findcard3  7811  unfilem1  7832  epfrs  8205  alephval3  8530  isfin7-2  8815  fin1a2lem6  8824  fpwwe2lem12  9055  fpwwe2lem13  9056  inawinalem  9103  ico0  11671  ioc0  11672  r19.2uz  13382  climrlim2  13578  iserodd  14737  ramub2  14923  prmgaplem6  14978  pgpssslw  17194  efgrelexlemb  17328  ablfaclem3  17648  unitgrp  17823  lspsneq  18273  lbsextlem4  18312  neissex  20067  iscnp4  20203  nlly2i  20415  llynlly  20416  restnlly  20421  llyrest  20424  nllyrest  20425  llyidm  20427  nllyidm  20428  qtophmeo  20756  cnpflfi  20938  cnextcn  21006  ivthlem3  22278  ovolicc2lem5  22349  dvfsumrlim  22857  itgsubst  22875  lgsquadlem2  24143  footex  24617  opphllem1  24643  oppperpex  24649  outpasch  24651  nbgraf1olem5  25015  cusgrafilem2  25050  cmppcmp  28521  eulerpartlemgvv  29032  eulerpartlemgh  29034  erdszelem7  29705  rellyscon  29759  trpredrec  30263  ivthALT  30773  fnessref  30795  phpreu  31633  poimirlem26  31670  itg2gt0cn  31701  frinfm  31766  sstotbnd2  31810  heiborlem3  31849  isdrngo3  31902  dihjat1lem  34705  dvh1dim  34719  dochsatshp  34728  lcfl6  34777  mapdval2N  34907  mapdpglem2  34950  hdmaprnlem10N  35139  pellexlem5  35387  pell14qrss1234  35412  pell1qrss14  35424  pellfundglb  35443  lnr2i  35685  hbtlem6  35698