MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdv2 Unicode version

Theorem reximdv2 2652
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
StepHypRef Expression
1 reximdv2.1 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  ->  ( x  e.  B  /\  ch ) ) )
21eximdv 1608 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2549 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2549 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43imtr4g 261 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  ssrexv  3238  nnsuc  4673  ssimaex  5584  oaass  6559  omeulem1  6580  ssnnfi  7082  findcard3  7100  unfilem1  7121  epfrs  7413  alephval3  7737  isfin7-2  8022  fin1a2lem6  8031  fpwwe2lem12  8263  fpwwe2lem13  8264  inawinalem  8311  ico0  10702  ioc0  10703  r19.2uz  11835  climrlim2  12021  iserodd  12888  ramub2  13061  pgpssslw  14925  efgrelexlemb  15059  ablfaclem3  15322  unitgrp  15449  lspsneq  15875  lbsextlem4  15914  neissex  16864  nlly2i  17202  llynlly  17203  restnlly  17208  llyrest  17211  nllyrest  17212  llyidm  17214  nllyidm  17215  qtophmeo  17508  cnpflfi  17694  ivthlem3  18813  ovolicc2lem5  18880  dvfsumrlim  19378  itgsubst  19396  lgsquadlem2  20594  erdszelem7  23728  rellyscon  23782  trpredrec  24241  iscnp4  25563  abhp  26173  ivthALT  26258  fnessref  26293  frinfm  26416  sstotbnd2  26498  heiborlem3  26537  isdrngo3  26590  pellexlem5  26918  pell14qrss1234  26941  pell1qrss14  26953  pellfundglb  26970  lnr2i  27320  hbtlem6  27333  climrec  27729  dihjat1lem  31618  dvh1dim  31632  dochsatshp  31641  lcfl6  31690  mapdval2N  31820  mapdpglem2  31863  hdmaprnlem10N  32052
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator