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

Theorem rexlimdvaa 2624
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypothesis
Ref Expression
rexlimdvaa.1  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
Assertion
Ref Expression
rexlimdvaa  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdvaa
StepHypRef Expression
1 rexlimdvaa.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
21expr 375 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32rexlimdva 2623 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2176   E.wrex 2485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490
This theorem is referenced by:  rexlimddv  2628  nnsucuniel  6581  omp1eomlem  7196  ctmlemr  7210  mulgt0sr  7891  axpre-suploclemres  8014  cnegex  8250  receuap  8742  recapb  8744  rexanuz  11299  climcaucn  11662  fsumiun  11788  dvdsval2  12101  nninfctlemfo  12361  prmind2  12442  pcprmpw2  12656  pockthg  12680  dvdsrvald  13855  dvdsrd  13856  dvdsrex  13860  unitgrp  13878  isnzr2  13946  znunit  14421  tgcl  14536  neiint  14617  restopnb  14653  iscnp4  14690  blssexps  14901  blssex  14902  lgsne0  15515  lgsquadlem1  15554
  Copyright terms: Public domain W3C validator