Theorem reximdva 2646

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∃wrex 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527  df-rex 2528

This theorem is referenced by:  reximddv  2647  reximddv2  2649  dffo4  5830  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  prarloclemarch  7749  appdivnq  7894  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  archrecpr  7995  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemladdfu  8008  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemlub  8055  archsr  8113  suplocsrlemb  8137  suplocsrlempr  8138  cnegexlem2  8465  bndndx  9512  elpq  9999  qbtwnxr  10641  expnbnd  11050  expnlbnd2  11052  caucvgre  11691  cvg1nlemres  11695  r19.29uz  11702  resqrexlemglsq  11732  resqrexlemga  11733  cau3lem  11824  qdenre  11912  2clim  12011  climcn1  12018  climcn2  12019  climsqz  12045  climsqz2  12046  climcau  12057  divcnv  12208  divalglemex  12633  dvdsbnd  12677  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlembi  12726  lcmgcdlem  12799  divgcdcoprmex  12824  exprmfct  12860  prmdvdsfz  12861  pclemub  13010  pc2dvds  13053  pcprmpw  13057  dvdsprmpweqle  13060  infpnlem2  13083  prmunb  13085  ennnfonelemhom  13250  ctinf  13265  sgrpidmndm  13717  grpinveu  13835  dfgrp3mlem  13895  ringadd2  14255  znunit  14919  cnpnei  15196  txlm  15256  metequiv2  15473  metrest  15483  mulc1cncf  15566  cncfco  15568  dedekindeulemlu  15598  suplociccreex  15601  dedekindicclemlu  15607  ivthinc  15620  cnplimcim  15644  cnplimclemr  15646  limccnpcntop  15652  limccoap  15655  elply2  15712  clwwlkn1loopb  16527  subctctexmid  16886