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

Theorem reximdv2 2783
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 1629 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2680 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2680 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43imtr4g 262 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547    e. wcel 1721   E.wrex 2675
This theorem is referenced by:  ssrexv  3376  nnsuc  4829  ssimaex  5755  oaass  6771  omeulem1  6792  ssnnfi  7295  findcard3  7317  unfilem1  7338  epfrs  7631  alephval3  7955  isfin7-2  8240  fin1a2lem6  8249  fpwwe2lem12  8480  fpwwe2lem13  8481  inawinalem  8528  ico0  10926  ioc0  10927  r19.2uz  12118  climrlim2  12304  iserodd  13172  ramub2  13345  pgpssslw  15211  efgrelexlemb  15345  ablfaclem3  15608  unitgrp  15735  lspsneq  16157  lbsextlem4  16196  neissex  17154  iscnp4  17289  nlly2i  17500  llynlly  17501  restnlly  17506  llyrest  17509  nllyrest  17510  llyidm  17512  nllyidm  17513  qtophmeo  17810  cnpflfi  17992  cnextcn  18059  ivthlem3  19311  ovolicc2lem5  19378  dvfsumrlim  19876  itgsubst  19894  lgsquadlem2  21100  nbgraf1olem5  21416  cusgrafilem2  21450  erdszelem7  24844  rellyscon  24899  trpredrec  25463  itg2gt0cn  26167  ivthALT  26236  fnessref  26271  frinfm  26335  sstotbnd2  26381  heiborlem3  26420  isdrngo3  26473  pellexlem5  26794  pell14qrss1234  26817  pell1qrss14  26829  pellfundglb  26846  lnr2i  27196  hbtlem6  27209  dihjat1lem  31923  dvh1dim  31937  dochsatshp  31946  lcfl6  31995  mapdval2N  32125  mapdpglem2  32168  hdmaprnlem10N  32357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-rex 2680
  Copyright terms: Public domain W3C validator