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

Theorem reximdv2 2654
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 1610 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2551 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2551 . 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 1530    e. wcel 1686   E.wrex 2546
This theorem is referenced by:  ssrexv  3240  nnsuc  4675  ssimaex  5586  oaass  6561  omeulem1  6582  ssnnfi  7084  findcard3  7102  unfilem1  7123  epfrs  7415  alephval3  7739  isfin7-2  8024  fin1a2lem6  8033  fpwwe2lem12  8265  fpwwe2lem13  8266  inawinalem  8313  ico0  10704  ioc0  10705  r19.2uz  11837  climrlim2  12023  iserodd  12890  ramub2  13063  pgpssslw  14927  efgrelexlemb  15061  ablfaclem3  15324  unitgrp  15451  lspsneq  15877  lbsextlem4  15916  neissex  16866  nlly2i  17204  llynlly  17205  restnlly  17210  llyrest  17213  nllyrest  17214  llyidm  17216  nllyidm  17217  qtophmeo  17510  cnpflfi  17696  ivthlem3  18815  ovolicc2lem5  18882  dvfsumrlim  19380  itgsubst  19398  lgsquadlem2  20596  erdszelem7  23730  rellyscon  23784  trpredrec  24243  iscnp4  25574  abhp  26184  ivthALT  26269  fnessref  26304  frinfm  26427  sstotbnd2  26509  heiborlem3  26548  isdrngo3  26601  pellexlem5  26929  pell14qrss1234  26952  pell1qrss14  26964  pellfundglb  26981  lnr2i  27331  hbtlem6  27344  climrec  27740  dihjat1lem  31691  dvh1dim  31705  dochsatshp  31714  lcfl6  31763  mapdval2N  31893  mapdpglem2  31936  hdmaprnlem10N  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605
This theorem depends on definitions:  df-bi 177  df-ex 1531  df-rex 2551
  Copyright terms: Public domain W3C validator