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

Theorem reximdv2 2807
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 1632 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  ->  E. x
( x  e.  B  /\  ch ) ) )
3 df-rex 2703 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2703 . 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 1550    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  ssrexv  3400  nnsuc  4854  ssimaex  5780  oaass  6796  omeulem1  6817  ssnnfi  7320  findcard3  7342  unfilem1  7363  epfrs  7659  alephval3  7983  isfin7-2  8268  fin1a2lem6  8277  fpwwe2lem12  8508  fpwwe2lem13  8509  inawinalem  8556  ico0  10954  ioc0  10955  r19.2uz  12147  climrlim2  12333  iserodd  13201  ramub2  13374  pgpssslw  15240  efgrelexlemb  15374  ablfaclem3  15637  unitgrp  15764  lspsneq  16186  lbsextlem4  16225  neissex  17183  iscnp4  17319  nlly2i  17531  llynlly  17532  restnlly  17537  llyrest  17540  nllyrest  17541  llyidm  17543  nllyidm  17544  qtophmeo  17841  cnpflfi  18023  cnextcn  18090  ivthlem3  19342  ovolicc2lem5  19409  dvfsumrlim  19907  itgsubst  19925  lgsquadlem2  21131  nbgraf1olem5  21447  cusgrafilem2  21481  erdszelem7  24875  rellyscon  24930  trpredrec  25508  itg2gt0cn  26250  ivthALT  26329  fnessref  26364  frinfm  26428  sstotbnd2  26474  heiborlem3  26513  isdrngo3  26566  pellexlem5  26887  pell14qrss1234  26910  pell1qrss14  26922  pellfundglb  26939  lnr2i  27288  hbtlem6  27301  dihjat1lem  32163  dvh1dim  32177  dochsatshp  32186  lcfl6  32235  mapdval2N  32365  mapdpglem2  32408  hdmaprnlem10N  32597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-rex 2703
  Copyright terms: Public domain W3C validator