Theorem reximdva 2609

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 2607	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  reximddv  2610  reximddv2  2612  dffo4  5738  ctm  7223  ctssdclemn0  7224  ctssdccl  7225  ctssdc  7227  prarloclemarch  7544  appdivnq  7689  ltexprlemm  7726  ltexprlemopl  7727  ltexprlemopu  7729  ltexprlemloc  7733  archpr  7769  cauappcvgprlemm  7771  cauappcvgprlemopl  7772  cauappcvgprlemlol  7773  cauappcvgprlemopu  7774  cauappcvgprlemladdfu  7780  cauappcvgprlemladdfl  7781  archrecpr  7790  caucvgprlemm  7794  caucvgprlemopl  7795  caucvgprlemlol  7796  caucvgprlemopu  7797  caucvgprlemladdfu  7803  caucvgprlemlim  7807  caucvgprprlemml  7820  caucvgprprlemopl  7823  caucvgprprlemlol  7824  caucvgprprlemopu  7825  caucvgprprlemexbt  7832  caucvgprprlemlim  7837  suplocexprlemmu  7844  suplocexprlemru  7845  suplocexprlemlub  7850  archsr  7908  suplocsrlemb  7932  suplocsrlempr  7933  cnegexlem2  8261  bndndx  9307  elpq  9783  qbtwnxr  10413  expnbnd  10821  expnlbnd2  10823  caucvgre  11342  cvg1nlemres  11346  r19.29uz  11353  resqrexlemglsq  11383  resqrexlemga  11384  cau3lem  11475  qdenre  11563  2clim  11662  climcn1  11669  climcn2  11670  climsqz  11696  climsqz2  11697  climcau  11708  divcnv  11858  divalglemex  12283  dvdsbnd  12327  bezoutlemzz  12373  bezoutlemaz  12374  bezoutlembz  12375  bezoutlembi  12376  lcmgcdlem  12449  divgcdcoprmex  12474  exprmfct  12510  prmdvdsfz  12511  pclemub  12660  pc2dvds  12703  pcprmpw  12707  dvdsprmpweqle  12710  infpnlem2  12733  prmunb  12735  ennnfonelemhom  12836  ctinf  12851  sgrpidmndm  13302  grpinveu  13420  dfgrp3mlem  13480  ringadd2  13839  znunit  14471  cnpnei  14741  txlm  14801  metequiv2  15018  metrest  15028  mulc1cncf  15111  cncfco  15113  dedekindeulemlu  15143  suplociccreex  15146  dedekindicclemlu  15152  ivthinc  15165  cnplimcim  15189  cnplimclemr  15191  limccnpcntop  15197  limccoap  15200  elply2  15257  subctctexmid  16052