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

Theorem reximdv 2591
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 2590 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  wrex 2469
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474
This theorem is referenced by:  r19.12  2596  reusv3  4478  rexxfrd  4481  iunpw  4498  fvelima  5588  carden2bex  7219  prnmaddl  7520  prarloclem5  7530  prarloc2  7534  genprndl  7551  genprndu  7552  ltpopr  7625  recexprlemm  7654  recexprlemopl  7655  recexprlemopu  7657  recexprlem1ssl  7663  recexprlem1ssu  7664  cauappcvgprlemupu  7679  caucvgprlemupu  7702  caucvgprprlemupu  7730  caucvgsrlemoffres  7830  map2psrprg  7835  resqrexlemgt0  11064  subcn2  11354  bezoutlembz  12040  pythagtriplem19  12317  tgcl  14041  neiss  14127  ssnei2  14134  tgcnp  14186  cnptopco  14199  cnptopresti  14215  lmtopcnp  14227  blssexps  14406  blssex  14407  mopni3  14461  neibl  14468  metss  14471  metcnp3  14488  rescncf  14545  limcresi  14612
  Copyright terms: Public domain W3C validator