Theorem reximdva 2634

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  reximddv  2635  reximddv2  2637  dffo4  5795  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  prarloclemarch  7638  appdivnq  7783  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  archrecpr  7884  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemladdfu  7897  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemlub  7944  archsr  8002  suplocsrlemb  8026  suplocsrlempr  8027  cnegexlem2  8355  bndndx  9401  elpq  9883  qbtwnxr  10518  expnbnd  10926  expnlbnd2  10928  caucvgre  11546  cvg1nlemres  11550  r19.29uz  11557  resqrexlemglsq  11587  resqrexlemga  11588  cau3lem  11679  qdenre  11767  2clim  11866  climcn1  11873  climcn2  11874  climsqz  11900  climsqz2  11901  climcau  11912  divcnv  12063  divalglemex  12488  dvdsbnd  12532  bezoutlemzz  12578  bezoutlemaz  12579  bezoutlembz  12580  bezoutlembi  12581  lcmgcdlem  12654  divgcdcoprmex  12679  exprmfct  12715  prmdvdsfz  12716  pclemub  12865  pc2dvds  12908  pcprmpw  12912  dvdsprmpweqle  12915  infpnlem2  12938  prmunb  12940  ennnfonelemhom  13041  ctinf  13056  sgrpidmndm  13508  grpinveu  13626  dfgrp3mlem  13686  ringadd2  14046  znunit  14679  cnpnei  14949  txlm  15009  metequiv2  15226  metrest  15236  mulc1cncf  15319  cncfco  15321  dedekindeulemlu  15351  suplociccreex  15354  dedekindicclemlu  15360  ivthinc  15373  cnplimcim  15397  cnplimclemr  15399  limccnpcntop  15405  limccoap  15408  elply2  15465  clwwlkn1loopb  16277  subctctexmid  16627