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

Theorem reximdv 2435
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 2434 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1407  wrex 2322
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-ral 2326  df-rex 2327
This theorem is referenced by:  r19.12  2437  reusv3  4217  rexxfrd  4220  iunpw  4236  fvelima  5250  carden2bex  6397  prnmaddl  6616  prarloclem5  6626  prarloc2  6630  genprndl  6647  genprndu  6648  ltpopr  6721  recexprlemm  6750  recexprlemopl  6751  recexprlemopu  6753  recexprlem1ssl  6759  recexprlem1ssu  6760  cauappcvgprlemupu  6775  caucvgprlemupu  6798  caucvgprprlemupu  6826  caucvgsrlemoffres  6912  resqrexlemgt0  9810  subcn2  10026
  Copyright terms: Public domain W3C validator