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

Theorem reximdva 2438
 Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
reximdva (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 112 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2436 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∈ wcel 1409  ∃wrex 2324 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 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443 This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329 This theorem is referenced by:  dffo4  5343  prarloclemarch  6574  appdivnq  6719  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemloc  6763  archpr  6799  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemopu  6804  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  archrecpr  6820  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemopu  6827  caucvgprlemladdfu  6833  caucvgprlemlim  6837  caucvgprprlemml  6850  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemexbt  6862  caucvgprprlemlim  6867  archsr  6924  cnegexlem2  7250  bndndx  8238  qbtwnxr  9214  expnbnd  9540  expnlbnd2  9542  caucvgre  9808  cvg1nlemres  9812  r19.29uz  9819  resqrexlemglsq  9849  resqrexlemga  9850  cau3lem  9941  qdenre  10029  2clim  10053  climcn1  10060  climcn2  10061  climsqz  10086  climsqz2  10087  climcau  10097  divalglemex  10234
 Copyright terms: Public domain W3C validator