Theorem reximdva 2596

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  ∃wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  reximddv  2597  reximddv2  2599  dffo4  5706  ctm  7168  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  prarloclemarch  7478  appdivnq  7623  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemloc  7667  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  archrecpr  7724  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemladdfu  7737  caucvgprlemlim  7741  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemexbt  7766  caucvgprprlemlim  7771  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemlub  7784  archsr  7842  suplocsrlemb  7866  suplocsrlempr  7867  cnegexlem2  8195  bndndx  9239  elpq  9714  qbtwnxr  10326  expnbnd  10734  expnlbnd2  10736  caucvgre  11125  cvg1nlemres  11129  r19.29uz  11136  resqrexlemglsq  11166  resqrexlemga  11167  cau3lem  11258  qdenre  11346  2clim  11444  climcn1  11451  climcn2  11452  climsqz  11478  climsqz2  11479  climcau  11490  divcnv  11640  divalglemex  12063  dvdsbnd  12093  bezoutlemzz  12139  bezoutlemaz  12140  bezoutlembz  12141  bezoutlembi  12142  lcmgcdlem  12215  divgcdcoprmex  12240  exprmfct  12276  prmdvdsfz  12277  pclemub  12425  pc2dvds  12468  pcprmpw  12472  dvdsprmpweqle  12475  infpnlem2  12498  prmunb  12500  ennnfonelemhom  12572  ctinf  12587  sgrpidmndm  13001  grpinveu  13110  dfgrp3mlem  13170  ringadd2  13523  znunit  14147  cnpnei  14387  txlm  14447  metequiv2  14664  metrest  14674  mulc1cncf  14744  cncfco  14746  dedekindeulemlu  14775  suplociccreex  14778  dedekindicclemlu  14784  ivthinc  14797  cnplimcim  14821  cnplimclemr  14823  limccnpcntop  14829  limccoap  14832  elply2  14881  subctctexmid  15491