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

Theorem reximdv2 2817
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 1633 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2713 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2713 . 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 4    /\ wa 360   E.wex 1551    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  ssrexv  3410  nnsuc  4864  ssimaex  5790  oaass  6806  omeulem1  6827  ssnnfi  7330  findcard3  7352  unfilem1  7373  epfrs  7669  alephval3  7993  isfin7-2  8278  fin1a2lem6  8287  fpwwe2lem12  8518  fpwwe2lem13  8519  inawinalem  8566  ico0  10964  ioc0  10965  r19.2uz  12157  climrlim2  12343  iserodd  13211  ramub2  13384  pgpssslw  15250  efgrelexlemb  15384  ablfaclem3  15647  unitgrp  15774  lspsneq  16196  lbsextlem4  16235  neissex  17193  iscnp4  17329  nlly2i  17541  llynlly  17542  restnlly  17547  llyrest  17550  nllyrest  17551  llyidm  17553  nllyidm  17554  qtophmeo  17851  cnpflfi  18033  cnextcn  18100  ivthlem3  19352  ovolicc2lem5  19419  dvfsumrlim  19917  itgsubst  19935  lgsquadlem2  21141  nbgraf1olem5  21457  cusgrafilem2  21491  erdszelem7  24885  rellyscon  24940  trpredrec  25518  itg2gt0cn  26262  ivthALT  26340  fnessref  26375  frinfm  26439  sstotbnd2  26485  heiborlem3  26524  isdrngo3  26577  pellexlem5  26898  pell14qrss1234  26921  pell1qrss14  26933  pellfundglb  26950  lnr2i  27299  hbtlem6  27312  dihjat1lem  32288  dvh1dim  32302  dochsatshp  32311  lcfl6  32360  mapdval2N  32490  mapdpglem2  32533  hdmaprnlem10N  32722
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-rex 2713
  Copyright terms: Public domain W3C validator