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

Theorem reximdv 2463
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 2462 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    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:  r19.12  2467  reusv3  4218  rexxfrd  4221  iunpw  4237  fvelima  5257  carden2bex  6517  prnmaddl  6742  prarloclem5  6752  prarloc2  6756  genprndl  6773  genprndu  6774  ltpopr  6847  recexprlemm  6876  recexprlemopl  6877  recexprlemopu  6879  recexprlem1ssl  6885  recexprlem1ssu  6886  cauappcvgprlemupu  6901  caucvgprlemupu  6924  caucvgprprlemupu  6952  caucvgsrlemoffres  7038  resqrexlemgt0  10044  subcn2  10288  bezoutlembz  10537
  Copyright terms: Public domain W3C validator