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

Theorem rexlimdvaa 2595
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypothesis
Ref Expression
rexlimdvaa.1 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimdvaa (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvaa
StepHypRef Expression
1 rexlimdvaa.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
21expr 375 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rexlimdva 2594 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461
This theorem is referenced by:  rexlimddv  2599  nnsucuniel  6490  omp1eomlem  7087  ctmlemr  7101  mulgt0sr  7765  axpre-suploclemres  7888  cnegex  8122  receuap  8612  recapb  8614  rexanuz  10978  climcaucn  11340  fsumiun  11466  dvdsval2  11778  prmind2  12100  pcprmpw2  12312  pockthg  12335  dvdsrvald  13084  dvdsrd  13085  dvdsrex  13089  unitgrp  13107  tgcl  13224  neiint  13305  restopnb  13341  iscnp4  13378  blssexps  13589  blssex  13590  lgsne0  14099
  Copyright terms: Public domain W3C validator