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

Theorem reximdv2 2653
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 2550 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2550 . 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 1685   E.wrex 2545
This theorem is referenced by:  ssrexv  3239  nnsuc  4672  ssimaex  5546  oaass  6555  omeulem1  6576  ssnnfi  7078  findcard3  7096  unfilem1  7117  epfrs  7409  alephval3  7733  isfin7-2  8018  fin1a2lem6  8027  fpwwe2lem12  8259  fpwwe2lem13  8260  inawinalem  8307  ico0  10698  ioc0  10699  r19.2uz  11831  climrlim2  12017  iserodd  12884  ramub2  13057  pgpssslw  14921  efgrelexlemb  15055  ablfaclem3  15318  unitgrp  15445  lspsneq  15871  lbsextlem4  15910  neissex  16860  nlly2i  17198  llynlly  17199  restnlly  17204  llyrest  17207  nllyrest  17208  llyidm  17210  nllyidm  17211  qtophmeo  17504  cnpflfi  17690  ivthlem3  18809  ovolicc2lem5  18876  dvfsumrlim  19374  itgsubst  19392  lgsquadlem2  20590  erdszelem7  23135  rellyscon  23189  trpredrec  23645  iscnp4  24974  abhp  25584  ivthALT  25669  fnessref  25704  frinfm  25827  sstotbnd2  25909  heiborlem3  25948  isdrngo3  26001  pellexlem5  26329  pell14qrss1234  26352  pell1qrss14  26364  pellfundglb  26381  lnr2i  26731  hbtlem6  26744  climrec  27140  dihjat1lem  30897  dvh1dim  30911  dochsatshp  30920  lcfl6  30969  mapdval2N  31099  mapdpglem2  31142  hdmaprnlem10N  31331
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 2550
  Copyright terms: Public domain W3C validator