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

Theorem reximdv 2492
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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
reximdv (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2491 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1448  wrex 2376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380  df-rex 2381
This theorem is referenced by:  r19.12  2497  reusv3  4319  rexxfrd  4322  iunpw  4339  fvelima  5405  carden2bex  6956  prnmaddl  7199  prarloclem5  7209  prarloc2  7213  genprndl  7230  genprndu  7231  ltpopr  7304  recexprlemm  7333  recexprlemopl  7334  recexprlemopu  7336  recexprlem1ssl  7342  recexprlem1ssu  7343  cauappcvgprlemupu  7358  caucvgprlemupu  7381  caucvgprprlemupu  7409  caucvgsrlemoffres  7495  resqrexlemgt0  10632  subcn2  10919  bezoutlembz  11485  tgcl  12015  neiss  12101  ssnei2  12108  tgcnp  12159  cnptopco  12172  cnptopresti  12188  lmtopcnp  12200  blssexps  12357  blssex  12358  mopni3  12412  neibl  12419  metss  12422  metcnp3  12435  rescncf  12481  limcresi  12515
  Copyright terms: Public domain W3C validator