Theorem reximdva 2632

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  reximddv  2633  reximddv2  2635  dffo4  5791  ctm  7302  ctssdclemn0  7303  ctssdccl  7304  ctssdc  7306  prarloclemarch  7631  appdivnq  7776  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemloc  7820  archpr  7856  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  archrecpr  7877  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemladdfu  7890  caucvgprlemlim  7894  caucvgprprlemml  7907  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemexbt  7919  caucvgprprlemlim  7924  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemlub  7937  archsr  7995  suplocsrlemb  8019  suplocsrlempr  8020  cnegexlem2  8348  bndndx  9394  elpq  9876  qbtwnxr  10510  expnbnd  10918  expnlbnd2  10920  caucvgre  11535  cvg1nlemres  11539  r19.29uz  11546  resqrexlemglsq  11576  resqrexlemga  11577  cau3lem  11668  qdenre  11756  2clim  11855  climcn1  11862  climcn2  11863  climsqz  11889  climsqz2  11890  climcau  11901  divcnv  12051  divalglemex  12476  dvdsbnd  12520  bezoutlemzz  12566  bezoutlemaz  12567  bezoutlembz  12568  bezoutlembi  12569  lcmgcdlem  12642  divgcdcoprmex  12667  exprmfct  12703  prmdvdsfz  12704  pclemub  12853  pc2dvds  12896  pcprmpw  12900  dvdsprmpweqle  12903  infpnlem2  12926  prmunb  12928  ennnfonelemhom  13029  ctinf  13044  sgrpidmndm  13496  grpinveu  13614  dfgrp3mlem  13674  ringadd2  14033  znunit  14666  cnpnei  14936  txlm  14996  metequiv2  15213  metrest  15223  mulc1cncf  15306  cncfco  15308  dedekindeulemlu  15338  suplociccreex  15341  dedekindicclemlu  15347  ivthinc  15360  cnplimcim  15384  cnplimclemr  15386  limccnpcntop  15392  limccoap  15395  elply2  15452  clwwlkn1loopb  16229  subctctexmid  16551