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  5859  ctm  7456  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  prarloclemarch  7792  appdivnq  7937  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemloc  7981  archpr  8017  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  archrecpr  8038  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemladdfu  8051  caucvgprlemlim  8055  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemexbt  8080  caucvgprprlemlim  8085  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemlub  8098  archsr  8156  suplocsrlemb  8180  suplocsrlempr  8181  cnegexlem2  8510  bndndx  9574  elpq  10067  qbtwnxr  10710  expnbnd  11123  expnlbnd2  11125  caucvgre  11770  cvg1nlemres  11774  r19.29uz  11781  resqrexlemglsq  11811  resqrexlemga  11812  cau3lem  11904  qdenre  11992  2clim  12093  climcn1  12100  climcn2  12101  climsqz  12127  climsqz2  12128  climcau  12139  divcnv  12290  divalglemex  12715  dvdsbnd  12759  bezoutlemzz  12805  bezoutlemaz  12806  bezoutlembz  12807  bezoutlembi  12808  lcmgcdlem  12881  divgcdcoprmex  12906  exprmfct  12943  prmdvdsfz  12944  pclemub  13096  pc2dvds  13139  pcprmpw  13143  dvdsprmpweqle  13146  infpnlem2  13169  prmunb  13171  ennnfonelemhom  13365  ctinf  13380  sgrpidmndm  13793  grpinveu  13903  dfgrp3mlem  13963  ringadd2  14440  znunit  15104  cnpnei  15457  txlm  15517  metequiv2  15734  metrest  15744  mulc1cncf  15827  cncfco  15829  dedekindeulemlu  15859  suplociccreex  15862  dedekindicclemlu  15868  ivthinc  15881  cnplimcim  15905  cnplimclemr  15907  limccnpcntop  15913  limccoap  15916  elply2  15973  clwwlkn1loopb  16878  subctctexmid  17247