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

Theorem reximdv2 2627
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 2019 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2524 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2524 . 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 2519
This theorem is referenced by:  ssrexv  3213  nnsuc  4645  ssimaex  5518  oaass  6527  omeulem1  6548  ssnnfi  7050  findcard3  7068  unfilem1  7089  epfrs  7381  alephval3  7705  isfin7-2  7990  fin1a2lem6  7999  fpwwe2lem12  8231  fpwwe2lem13  8232  inawinalem  8279  ico0  10669  ioc0  10670  r19.2uz  11801  climrlim2  11987  iserodd  12851  ramub2  13024  pgpssslw  14888  efgrelexlemb  15022  ablfaclem3  15285  unitgrp  15412  lspsneq  15838  lbsextlem4  15877  neissex  16827  nlly2i  17165  llynlly  17166  restnlly  17171  llyrest  17174  nllyrest  17175  llyidm  17177  nllyidm  17178  qtophmeo  17471  cnpflfi  17657  ivthlem3  18776  ovolicc2lem5  18843  dvfsumrlim  19341  itgsubst  19359  lgsquadlem2  20557  erdszelem7  23101  rellyscon  23155  trpredrec  23611  iscnp4  24931  abhp  25541  ivthALT  25626  fnessref  25661  frinfm  25784  sstotbnd2  25866  heiborlem3  25905  isdrngo3  25958  pellexlem5  26286  pell14qrss1234  26309  pell1qrss14  26321  pellfundglb  26338  lnr2i  26688  hbtlem6  26701  climrec  27098  dihjat1lem  30868  dvh1dim  30882  dochsatshp  30891  lcfl6  30940  mapdval2N  31070  mapdpglem2  31113  hdmaprnlem10N  31302
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 2524
  Copyright terms: Public domain W3C validator