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  8466  bndndx  9515  elpq  10002  qbtwnxr  10644  expnbnd  11053  expnlbnd2  11055  caucvgre  11695  cvg1nlemres  11699  r19.29uz  11706  resqrexlemglsq  11736  resqrexlemga  11737  cau3lem  11828  qdenre  11916  2clim  12015  climcn1  12022  climcn2  12023  climsqz  12049  climsqz2  12050  climcau  12061  divcnv  12212  divalglemex  12637  dvdsbnd  12681  bezoutlemzz  12727  bezoutlemaz  12728  bezoutlembz  12729  bezoutlembi  12730  lcmgcdlem  12803  divgcdcoprmex  12828  exprmfct  12864  prmdvdsfz  12865  pclemub  13014  pc2dvds  13057  pcprmpw  13061  dvdsprmpweqle  13064  infpnlem2  13087  prmunb  13089  ennnfonelemhom  13254  ctinf  13269  sgrpidmndm  13685  grpinveu  13797  dfgrp3mlem  13857  ringadd2  14274  znunit  14937  cnpnei  15214  txlm  15274  metequiv2  15491  metrest  15501  mulc1cncf  15584  cncfco  15586  dedekindeulemlu  15616  suplociccreex  15619  dedekindicclemlu  15625  ivthinc  15638  cnplimcim  15662  cnplimclemr  15664  limccnpcntop  15670  limccoap  15673  elply2  15730  clwwlkn1loopb  16545  subctctexmid  16914