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

Theorem reximdva 2464
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 113 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2462 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1434   E.wrex 2350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354  df-rex 2355
This theorem is referenced by:  reximddv  2465  reximddv2  2466  dffo4  5347  prarloclemarch  6670  appdivnq  6815  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemloc  6859  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  archrecpr  6916  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemladdfu  6929  caucvgprlemlim  6933  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemexbt  6958  caucvgprprlemlim  6963  archsr  7020  cnegexlem2  7351  bndndx  8354  qbtwnxr  9344  expnbnd  9693  expnlbnd2  9695  caucvgre  10005  cvg1nlemres  10009  r19.29uz  10016  resqrexlemglsq  10046  resqrexlemga  10047  cau3lem  10138  qdenre  10226  2clim  10278  climcn1  10285  climcn2  10286  climsqz  10311  climsqz2  10312  climcau  10322  divalglemex  10466  dvdsbnd  10492  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlembi  10538  lcmgcdlem  10603  divgcdcoprmex  10628  exprmfct  10663  prmdvdsfz  10664
  Copyright terms: Public domain W3C validator