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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

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

This theorem is referenced by:  reximddv  2653  reximddv2  2655  dffo4  5850  ctm  7443  ctssdclemn0  7444  ctssdccl  7445  ctssdc  7447  prarloclemarch  7779  appdivnq  7924  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemloc  7968  archpr  8004  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  archrecpr  8025  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemladdfu  8038  caucvgprlemlim  8042  caucvgprprlemml  8055  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemexbt  8067  caucvgprprlemlim  8072  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemlub  8085  archsr  8143  suplocsrlemb  8167  suplocsrlempr  8168  cnegexlem2  8496  bndndx  9545  elpq  10032  qbtwnxr  10675  expnbnd  11084  expnlbnd2  11086  caucvgre  11730  cvg1nlemres  11734  r19.29uz  11741  resqrexlemglsq  11771  resqrexlemga  11772  cau3lem  11863  qdenre  11951  2clim  12050  climcn1  12057  climcn2  12058  climsqz  12084  climsqz2  12085  climcau  12096  divcnv  12247  divalglemex  12672  dvdsbnd  12716  bezoutlemzz  12762  bezoutlemaz  12763  bezoutlembz  12764  bezoutlembi  12765  lcmgcdlem  12838  divgcdcoprmex  12863  exprmfct  12899  prmdvdsfz  12900  pclemub  13049  pc2dvds  13092  pcprmpw  13096  dvdsprmpweqle  13099  infpnlem2  13122  prmunb  13124  ennnfonelemhom  13289  ctinf  13304  sgrpidmndm  13716  grpinveu  13826  dfgrp3mlem  13886  ringadd2  14315  znunit  14977  cnpnei  15303  txlm  15363  metequiv2  15580  metrest  15590  mulc1cncf  15673  cncfco  15675  dedekindeulemlu  15705  suplociccreex  15708  dedekindicclemlu  15714  ivthinc  15727  cnplimcim  15751  cnplimclemr  15753  limccnpcntop  15759  limccoap  15762  elply2  15819  clwwlkn1loopb  16644  subctctexmid  17013