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

Theorem reximdva 2537
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 114 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 2535 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1481  wrex 2418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423
This theorem is referenced by:  reximddv  2538  reximddv2  2540  dffo4  5575  ctm  7001  ctssdclemn0  7002  ctssdccl  7003  ctssdc  7005  prarloclemarch  7249  appdivnq  7394  ltexprlemm  7431  ltexprlemopl  7432  ltexprlemopu  7434  ltexprlemloc  7438  archpr  7474  cauappcvgprlemm  7476  cauappcvgprlemopl  7477  cauappcvgprlemlol  7478  cauappcvgprlemopu  7479  cauappcvgprlemladdfu  7485  cauappcvgprlemladdfl  7486  archrecpr  7495  caucvgprlemm  7499  caucvgprlemopl  7500  caucvgprlemlol  7501  caucvgprlemopu  7502  caucvgprlemladdfu  7508  caucvgprlemlim  7512  caucvgprprlemml  7525  caucvgprprlemopl  7528  caucvgprprlemlol  7529  caucvgprprlemopu  7530  caucvgprprlemexbt  7537  caucvgprprlemlim  7542  suplocexprlemmu  7549  suplocexprlemru  7550  suplocexprlemlub  7555  archsr  7613  suplocsrlemb  7637  suplocsrlempr  7638  cnegexlem2  7961  bndndx  8999  elpq  9466  qbtwnxr  10065  expnbnd  10445  expnlbnd2  10447  caucvgre  10784  cvg1nlemres  10788  r19.29uz  10795  resqrexlemglsq  10825  resqrexlemga  10826  cau3lem  10917  qdenre  11005  2clim  11101  climcn1  11108  climcn2  11109  climsqz  11135  climsqz2  11136  climcau  11147  divcnv  11297  divalglemex  11653  dvdsbnd  11679  bezoutlemzz  11724  bezoutlemaz  11725  bezoutlembz  11726  bezoutlembi  11727  lcmgcdlem  11792  divgcdcoprmex  11817  exprmfct  11852  prmdvdsfz  11853  ennnfonelemhom  11962  ctinf  11977  cnpnei  12425  txlm  12485  metequiv2  12702  metrest  12712  mulc1cncf  12782  cncfco  12784  dedekindeulemlu  12805  suplociccreex  12808  dedekindicclemlu  12814  ivthinc  12827  cnplimcim  12842  cnplimclemr  12844  limccnpcntop  12850  limccoap  12853  subctctexmid  13367
  Copyright terms: Public domain W3C validator