Theorem reximdva 2599

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  reximddv  2600  reximddv2  2602  dffo4  5713  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  prarloclemarch  7502  appdivnq  7647  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemloc  7691  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  archrecpr  7748  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemladdfu  7761  caucvgprlemlim  7765  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemexbt  7790  caucvgprprlemlim  7795  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemlub  7808  archsr  7866  suplocsrlemb  7890  suplocsrlempr  7891  cnegexlem2  8219  bndndx  9265  elpq  9740  qbtwnxr  10364  expnbnd  10772  expnlbnd2  10774  caucvgre  11163  cvg1nlemres  11167  r19.29uz  11174  resqrexlemglsq  11204  resqrexlemga  11205  cau3lem  11296  qdenre  11384  2clim  11483  climcn1  11490  climcn2  11491  climsqz  11517  climsqz2  11518  climcau  11529  divcnv  11679  divalglemex  12104  dvdsbnd  12148  bezoutlemzz  12194  bezoutlemaz  12195  bezoutlembz  12196  bezoutlembi  12197  lcmgcdlem  12270  divgcdcoprmex  12295  exprmfct  12331  prmdvdsfz  12332  pclemub  12481  pc2dvds  12524  pcprmpw  12528  dvdsprmpweqle  12531  infpnlem2  12554  prmunb  12556  ennnfonelemhom  12657  ctinf  12672  sgrpidmndm  13122  grpinveu  13240  dfgrp3mlem  13300  ringadd2  13659  znunit  14291  cnpnei  14539  txlm  14599  metequiv2  14816  metrest  14826  mulc1cncf  14909  cncfco  14911  dedekindeulemlu  14941  suplociccreex  14944  dedekindicclemlu  14950  ivthinc  14963  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccoap  14998  elply2  15055  subctctexmid  15731