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

Theorem reximdv2 2623
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 2019 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2521 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2521 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43imtr4g 263 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1537    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  ssrexv  3180  nnsuc  4610  ssimaex  5483  oaass  6492  omeulem1  6513  ssnnfi  7015  findcard3  7033  unfilem1  7054  epfrs  7346  alephval3  7670  isfin7-2  7955  fin1a2lem6  7964  fpwwe2lem12  8196  fpwwe2lem13  8197  inawinalem  8244  ico0  10633  ioc0  10634  r19.2uz  11765  climrlim2  11951  iserodd  12815  ramub2  12988  pgpssslw  14852  efgrelexlemb  14986  ablfaclem3  15249  unitgrp  15376  lspsneq  15802  lbsextlem4  15841  neissex  16791  nlly2i  17129  llynlly  17130  restnlly  17135  llyrest  17138  nllyrest  17139  llyidm  17141  nllyidm  17142  qtophmeo  17435  cnpflfi  17621  ivthlem3  18740  ovolicc2lem5  18807  dvfsumrlim  19305  itgsubst  19323  lgsquadlem2  20521  erdszelem7  23065  rellyscon  23119  trpredrec  23575  iscnp4  24895  abhp  25505  ivthALT  25590  fnessref  25625  frinfm  25748  sstotbnd2  25830  heiborlem3  25869  isdrngo3  25922  pellexlem5  26250  pell14qrss1234  26273  pell1qrss14  26285  pellfundglb  26302  lnr2i  26652  hbtlem6  26665  dihjat1lem  30748  dvh1dim  30762  dochsatshp  30771  lcfl6  30820  mapdval2N  30950  mapdpglem2  30993  hdmaprnlem10N  31182
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-nf 1540  df-rex 2521
  Copyright terms: Public domain W3C validator