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  5785  ctm  7284  ctssdclemn0  7285  ctssdccl  7286  ctssdc  7288  prarloclemarch  7613  appdivnq  7758  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemloc  7802  archpr  7838  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  archrecpr  7859  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemladdfu  7872  caucvgprlemlim  7876  caucvgprprlemml  7889  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemexbt  7901  caucvgprprlemlim  7906  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemlub  7919  archsr  7977  suplocsrlemb  8001  suplocsrlempr  8002  cnegexlem2  8330  bndndx  9376  elpq  9852  qbtwnxr  10485  expnbnd  10893  expnlbnd2  10895  caucvgre  11500  cvg1nlemres  11504  r19.29uz  11511  resqrexlemglsq  11541  resqrexlemga  11542  cau3lem  11633  qdenre  11721  2clim  11820  climcn1  11827  climcn2  11828  climsqz  11854  climsqz2  11855  climcau  11866  divcnv  12016  divalglemex  12441  dvdsbnd  12485  bezoutlemzz  12531  bezoutlemaz  12532  bezoutlembz  12533  bezoutlembi  12534  lcmgcdlem  12607  divgcdcoprmex  12632  exprmfct  12668  prmdvdsfz  12669  pclemub  12818  pc2dvds  12861  pcprmpw  12865  dvdsprmpweqle  12868  infpnlem2  12891  prmunb  12893  ennnfonelemhom  12994  ctinf  13009  sgrpidmndm  13461  grpinveu  13579  dfgrp3mlem  13639  ringadd2  13998  znunit  14631  cnpnei  14901  txlm  14961  metequiv2  15178  metrest  15188  mulc1cncf  15271  cncfco  15273  dedekindeulemlu  15303  suplociccreex  15306  dedekindicclemlu  15312  ivthinc  15325  cnplimcim  15349  cnplimclemr  15351  limccnpcntop  15357  limccoap  15360  elply2  15417  subctctexmid  16395