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

Theorem reximdv2 2759
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 2656 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2656 . 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 1717   E.wrex 2651
This theorem is referenced by:  ssrexv  3352  nnsuc  4803  ssimaex  5728  oaass  6741  omeulem1  6762  ssnnfi  7265  findcard3  7287  unfilem1  7308  epfrs  7601  alephval3  7925  isfin7-2  8210  fin1a2lem6  8219  fpwwe2lem12  8450  fpwwe2lem13  8451  inawinalem  8498  ico0  10895  ioc0  10896  r19.2uz  12083  climrlim2  12269  iserodd  13137  ramub2  13310  pgpssslw  15176  efgrelexlemb  15310  ablfaclem3  15573  unitgrp  15700  lspsneq  16122  lbsextlem4  16161  neissex  17115  iscnp4  17250  nlly2i  17461  llynlly  17462  restnlly  17467  llyrest  17470  nllyrest  17471  llyidm  17473  nllyidm  17474  qtophmeo  17771  cnpflfi  17953  cnextcn  18020  ivthlem3  19218  ovolicc2lem5  19285  dvfsumrlim  19783  itgsubst  19801  lgsquadlem2  21007  nbgraf1olem5  21322  cusgrafilem2  21356  erdszelem7  24663  rellyscon  24718  trpredrec  25266  itg2gt0cn  25961  ivthALT  26030  fnessref  26065  frinfm  26129  sstotbnd2  26175  heiborlem3  26214  isdrngo3  26267  pellexlem5  26588  pell14qrss1234  26611  pell1qrss14  26623  pellfundglb  26640  lnr2i  26990  hbtlem6  27003  dihjat1lem  31544  dvh1dim  31558  dochsatshp  31567  lcfl6  31616  mapdval2N  31746  mapdpglem2  31789  hdmaprnlem10N  31978
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 2656
  Copyright terms: Public domain W3C validator