Theorem reximdva 2652

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  reximddv  2653  reximddv2  2655  dffo4  5856  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  prarloclemarch  7786  appdivnq  7931  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  archrecpr  8032  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemladdfu  8045  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemexbt  8074  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemlub  8092  archsr  8150  suplocsrlemb  8174  suplocsrlempr  8175  cnegexlem2  8504  bndndx  9567  elpq  10060  qbtwnxr  10703  expnbnd  11115  expnlbnd2  11117  caucvgre  11762  cvg1nlemres  11766  r19.29uz  11773  resqrexlemglsq  11803  resqrexlemga  11804  cau3lem  11896  qdenre  11984  2clim  12085  climcn1  12092  climcn2  12093  climsqz  12119  climsqz2  12120  climcau  12131  divcnv  12282  divalglemex  12707  dvdsbnd  12751  bezoutlemzz  12797  bezoutlemaz  12798  bezoutlembz  12799  bezoutlembi  12800  lcmgcdlem  12873  divgcdcoprmex  12898  exprmfct  12935  prmdvdsfz  12936  pclemub  13088  pc2dvds  13131  pcprmpw  13135  dvdsprmpweqle  13138  infpnlem2  13161  prmunb  13163  ennnfonelemhom  13357  ctinf  13372  sgrpidmndm  13784  grpinveu  13894  dfgrp3mlem  13954  ringadd2  14383  znunit  15045  cnpnei  15372  txlm  15432  metequiv2  15649  metrest  15659  mulc1cncf  15742  cncfco  15744  dedekindeulemlu  15774  suplociccreex  15777  dedekindicclemlu  15783  ivthinc  15796  cnplimcim  15820  cnplimclemr  15822  limccnpcntop  15828  limccoap  15831  elply2  15888  clwwlkn1loopb  16783  subctctexmid  17152