Theorem reximdva 2644

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

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 2642	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  reximddv  2645  reximddv2  2647  dffo4  5824  ctm  7399  ctssdclemn0  7400  ctssdccl  7401  ctssdc  7403  prarloclemarch  7732  appdivnq  7877  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemopu  7917  ltexprlemloc  7921  archpr  7957  cauappcvgprlemm  7959  cauappcvgprlemopl  7960  cauappcvgprlemlol  7961  cauappcvgprlemopu  7962  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  archrecpr  7978  caucvgprlemm  7982  caucvgprlemopl  7983  caucvgprlemlol  7984  caucvgprlemopu  7985  caucvgprlemladdfu  7991  caucvgprlemlim  7995  caucvgprprlemml  8008  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemopu  8013  caucvgprprlemexbt  8020  caucvgprprlemlim  8025  suplocexprlemmu  8032  suplocexprlemru  8033  suplocexprlemlub  8038  archsr  8096  suplocsrlemb  8120  suplocsrlempr  8121  cnegexlem2  8448  bndndx  9494  elpq  9980  qbtwnxr  10616  expnbnd  11024  expnlbnd2  11026  caucvgre  11662  cvg1nlemres  11666  r19.29uz  11673  resqrexlemglsq  11703  resqrexlemga  11704  cau3lem  11795  qdenre  11883  2clim  11982  climcn1  11989  climcn2  11990  climsqz  12016  climsqz2  12017  climcau  12028  divcnv  12179  divalglemex  12604  dvdsbnd  12648  bezoutlemzz  12694  bezoutlemaz  12695  bezoutlembz  12696  bezoutlembi  12697  lcmgcdlem  12770  divgcdcoprmex  12795  exprmfct  12831  prmdvdsfz  12832  pclemub  12981  pc2dvds  13024  pcprmpw  13028  dvdsprmpweqle  13031  infpnlem2  13054  prmunb  13056  ennnfonelemhom  13158  ctinf  13173  sgrpidmndm  13625  grpinveu  13743  dfgrp3mlem  13803  ringadd2  14163  znunit  14799  cnpnei  15076  txlm  15136  metequiv2  15353  metrest  15363  mulc1cncf  15446  cncfco  15448  dedekindeulemlu  15478  suplociccreex  15481  dedekindicclemlu  15487  ivthinc  15500  cnplimcim  15524  cnplimclemr  15526  limccnpcntop  15532  limccoap  15535  elply2  15592  clwwlkn1loopb  16407  subctctexmid  16766