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

Theorem reximdv2 2614
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 2018 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2514 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2514 . 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 2510
This theorem is referenced by:  ssrexv  3159  nnsuc  4564  ssimaex  5436  oaass  6445  omeulem1  6466  ssnnfi  6967  findcard3  6985  unfilem1  7006  epfrs  7297  alephval3  7621  isfin7-2  7906  fin1a2lem6  7915  fpwwe2lem12  8143  fpwwe2lem13  8144  inawinalem  8191  ico0  10580  ioc0  10581  r19.2uz  11712  climrlim2  11898  iserodd  12762  ramub2  12935  pgpssslw  14760  efgrelexlemb  14894  ablfaclem3  15157  unitgrp  15284  lspsneq  15710  lbsextlem4  15746  neissex  16696  nlly2i  17034  llynlly  17035  restnlly  17040  llyrest  17043  nllyrest  17044  llyidm  17046  nllyidm  17047  qtophmeo  17340  cnpflfi  17526  ivthlem3  18645  ovolicc2lem5  18712  dvfsumrlim  19210  itgsubst  19228  lgsquadlem2  20426  erdszelem7  22899  rellyscon  22953  trpredrec  23409  iscnp4  24729  abhp  25339  ivthALT  25424  fnessref  25459  frinfm  25582  sstotbnd2  25664  heiborlem3  25703  isdrngo3  25756  pellexlem5  26084  pell14qrss1234  26107  pell1qrss14  26119  pellfundglb  26136  lnr2i  26486  hbtlem6  26499  dihjat1lem  30307  dvh1dim  30321  dochsatshp  30330  lcfl6  30379  mapdval2N  30509  mapdpglem2  30552  hdmaprnlem10N  30741
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 2514
  Copyright terms: Public domain W3C validator