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

Theorem reximdva 2475
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 2473 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 1438   E.wrex 2360
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365
This theorem is referenced by:  reximddv  2476  reximddv2  2477  dffo4  5447  prarloclemarch  6977  appdivnq  7122  ltexprlemm  7159  ltexprlemopl  7160  ltexprlemopu  7162  ltexprlemloc  7166  archpr  7202  cauappcvgprlemm  7204  cauappcvgprlemopl  7205  cauappcvgprlemlol  7206  cauappcvgprlemopu  7207  cauappcvgprlemladdfu  7213  cauappcvgprlemladdfl  7214  archrecpr  7223  caucvgprlemm  7227  caucvgprlemopl  7228  caucvgprlemlol  7229  caucvgprlemopu  7230  caucvgprlemladdfu  7236  caucvgprlemlim  7240  caucvgprprlemml  7253  caucvgprprlemopl  7256  caucvgprprlemlol  7257  caucvgprprlemopu  7258  caucvgprprlemexbt  7265  caucvgprprlemlim  7270  archsr  7327  cnegexlem2  7658  bndndx  8672  qbtwnxr  9669  expnbnd  10077  expnlbnd2  10079  caucvgre  10414  cvg1nlemres  10418  r19.29uz  10425  resqrexlemglsq  10455  resqrexlemga  10456  cau3lem  10547  qdenre  10635  2clim  10689  climcn1  10697  climcn2  10698  climsqz  10723  climsqz2  10724  climcau  10736  divcnv  10891  divalglemex  11200  dvdsbnd  11226  bezoutlemzz  11269  bezoutlemaz  11270  bezoutlembz  11271  bezoutlembi  11272  lcmgcdlem  11337  divgcdcoprmex  11362  exprmfct  11397  prmdvdsfz  11398  mulc1cncf  11645  cncfco  11647
  Copyright terms: Public domain W3C validator