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

Theorem reximdv2 2665
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 1612 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2562 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2562 . 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 1531    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  ssrexv  3251  nnsuc  4689  ssimaex  5600  oaass  6575  omeulem1  6596  ssnnfi  7098  findcard3  7116  unfilem1  7137  epfrs  7429  alephval3  7753  isfin7-2  8038  fin1a2lem6  8047  fpwwe2lem12  8279  fpwwe2lem13  8280  inawinalem  8327  ico0  10718  ioc0  10719  r19.2uz  11851  climrlim2  12037  iserodd  12904  ramub2  13077  pgpssslw  14941  efgrelexlemb  15075  ablfaclem3  15338  unitgrp  15465  lspsneq  15891  lbsextlem4  15930  neissex  16880  nlly2i  17218  llynlly  17219  restnlly  17224  llyrest  17227  nllyrest  17228  llyidm  17230  nllyidm  17231  qtophmeo  17524  cnpflfi  17710  ivthlem3  18829  ovolicc2lem5  18896  dvfsumrlim  19394  itgsubst  19412  lgsquadlem2  20610  erdszelem7  23743  rellyscon  23797  trpredrec  24312  itg2gt0cn  25006  iscnp4  25666  abhp  26276  ivthALT  26361  fnessref  26396  frinfm  26519  sstotbnd2  26601  heiborlem3  26640  isdrngo3  26693  pellexlem5  27021  pell14qrss1234  27044  pell1qrss14  27056  pellfundglb  27073  lnr2i  27423  hbtlem6  27436  climrec  27832  dihjat1lem  32240  dvh1dim  32254  dochsatshp  32263  lcfl6  32312  mapdval2N  32442  mapdpglem2  32485  hdmaprnlem10N  32674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-rex 2562
  Copyright terms: Public domain W3C validator