Theorem reximdva 2632

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  reximddv  2633  reximddv2  2635  dffo4  5776  ctm  7264  ctssdclemn0  7265  ctssdccl  7266  ctssdc  7268  prarloclemarch  7593  appdivnq  7738  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemopu  7778  ltexprlemloc  7782  archpr  7818  cauappcvgprlemm  7820  cauappcvgprlemopl  7821  cauappcvgprlemlol  7822  cauappcvgprlemopu  7823  cauappcvgprlemladdfu  7829  cauappcvgprlemladdfl  7830  archrecpr  7839  caucvgprlemm  7843  caucvgprlemopl  7844  caucvgprlemlol  7845  caucvgprlemopu  7846  caucvgprlemladdfu  7852  caucvgprlemlim  7856  caucvgprprlemml  7869  caucvgprprlemopl  7872  caucvgprprlemlol  7873  caucvgprprlemopu  7874  caucvgprprlemexbt  7881  caucvgprprlemlim  7886  suplocexprlemmu  7893  suplocexprlemru  7894  suplocexprlemlub  7899  archsr  7957  suplocsrlemb  7981  suplocsrlempr  7982  cnegexlem2  8310  bndndx  9356  elpq  9832  qbtwnxr  10464  expnbnd  10872  expnlbnd2  10874  caucvgre  11478  cvg1nlemres  11482  r19.29uz  11489  resqrexlemglsq  11519  resqrexlemga  11520  cau3lem  11611  qdenre  11699  2clim  11798  climcn1  11805  climcn2  11806  climsqz  11832  climsqz2  11833  climcau  11844  divcnv  11994  divalglemex  12419  dvdsbnd  12463  bezoutlemzz  12509  bezoutlemaz  12510  bezoutlembz  12511  bezoutlembi  12512  lcmgcdlem  12585  divgcdcoprmex  12610  exprmfct  12646  prmdvdsfz  12647  pclemub  12796  pc2dvds  12839  pcprmpw  12843  dvdsprmpweqle  12846  infpnlem2  12869  prmunb  12871  ennnfonelemhom  12972  ctinf  12987  sgrpidmndm  13439  grpinveu  13557  dfgrp3mlem  13617  ringadd2  13976  znunit  14608  cnpnei  14878  txlm  14938  metequiv2  15155  metrest  15165  mulc1cncf  15248  cncfco  15250  dedekindeulemlu  15280  suplociccreex  15283  dedekindicclemlu  15289  ivthinc  15302  cnplimcim  15326  cnplimclemr  15328  limccnpcntop  15334  limccoap  15337  elply2  15394  subctctexmid  16297