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

Theorem reximdv 2474
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
Hypothesis
Ref Expression
reximdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
reximdv  |-  ( 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 reximdv
StepHypRef Expression
1 reximdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21a1d 22 . 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    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:  r19.12  2478  reusv3  4282  rexxfrd  4285  iunpw  4302  fvelima  5356  carden2bex  6817  prnmaddl  7049  prarloclem5  7059  prarloc2  7063  genprndl  7080  genprndu  7081  ltpopr  7154  recexprlemm  7183  recexprlemopl  7184  recexprlemopu  7186  recexprlem1ssl  7192  recexprlem1ssu  7193  cauappcvgprlemupu  7208  caucvgprlemupu  7231  caucvgprprlemupu  7259  caucvgsrlemoffres  7345  resqrexlemgt0  10453  subcn2  10700  bezoutlembz  11271  rescncf  11637
  Copyright terms: Public domain W3C validator