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  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  prarloclemarch  7785  appdivnq  7930  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  archrecpr  8031  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemladdfu  8044  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemlub  8091  archsr  8149  suplocsrlemb  8173  suplocsrlempr  8174  cnegexlem2  8502  bndndx  9564  elpq  10051  qbtwnxr  10694  expnbnd  11103  expnlbnd2  11105  caucvgre  11749  cvg1nlemres  11753  r19.29uz  11760  resqrexlemglsq  11790  resqrexlemga  11791  cau3lem  11882  qdenre  11970  2clim  12069  climcn1  12076  climcn2  12077  climsqz  12103  climsqz2  12104  climcau  12115  divcnv  12266  divalglemex  12691  dvdsbnd  12735  bezoutlemzz  12781  bezoutlemaz  12782  bezoutlembz  12783  bezoutlembi  12784  lcmgcdlem  12857  divgcdcoprmex  12882  exprmfct  12918  prmdvdsfz  12919  pclemub  13068  pc2dvds  13111  pcprmpw  13115  dvdsprmpweqle  13118  infpnlem2  13141  prmunb  13143  ennnfonelemhom  13308  ctinf  13323  sgrpidmndm  13735  grpinveu  13845  dfgrp3mlem  13905  ringadd2  14334  znunit  14996  cnpnei  15322  txlm  15382  metequiv2  15599  metrest  15609  mulc1cncf  15692  cncfco  15694  dedekindeulemlu  15724  suplociccreex  15727  dedekindicclemlu  15733  ivthinc  15746  cnplimcim  15770  cnplimclemr  15772  limccnpcntop  15778  limccoap  15781  elply2  15838  clwwlkn1loopb  16673  subctctexmid  17042