ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reximdva Unicode version

Theorem reximdva 2421
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
reximdva  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 108 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2419 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    e. wcel 1393   E.wrex 2307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312
This theorem is referenced by:  dffo4  5315  prarloclemarch  6516  appdivnq  6661  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  archrecpr  6762  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemladdfu  6775  caucvgprlemlim  6779  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemexbt  6804  caucvgprprlemlim  6809  archsr  6866  cnegexlem2  7187  bndndx  8180  expnbnd  9372  expnlbnd2  9374  caucvgre  9580  cvg1nlemres  9584  r19.29uz  9590  resqrexlemglsq  9620  resqrexlemga  9621  cau3lem  9710  qdenre  9798  2clim  9822  climcn1  9829  climcn2  9830  climsqz  9855  climsqz2  9856  climcau  9866
  Copyright terms: Public domain W3C validator