Theorem reximdva 2579

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  reximddv  2580  reximddv2  2582  dffo4  5664  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  prarloclemarch  7416  appdivnq  7561  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemloc  7605  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  archrecpr  7662  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemladdfu  7675  caucvgprlemlim  7679  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemexbt  7704  caucvgprprlemlim  7709  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemlub  7722  archsr  7780  suplocsrlemb  7804  suplocsrlempr  7805  cnegexlem2  8131  bndndx  9173  elpq  9646  qbtwnxr  10255  expnbnd  10640  expnlbnd2  10642  caucvgre  10985  cvg1nlemres  10989  r19.29uz  10996  resqrexlemglsq  11026  resqrexlemga  11027  cau3lem  11118  qdenre  11206  2clim  11304  climcn1  11311  climcn2  11312  climsqz  11338  climsqz2  11339  climcau  11350  divcnv  11500  divalglemex  11921  dvdsbnd  11951  bezoutlemzz  11997  bezoutlemaz  11998  bezoutlembz  11999  bezoutlembi  12000  lcmgcdlem  12071  divgcdcoprmex  12096  exprmfct  12132  prmdvdsfz  12133  pclemub  12281  pc2dvds  12323  pcprmpw  12327  dvdsprmpweqle  12330  infpnlem2  12352  prmunb  12354  ennnfonelemhom  12410  ctinf  12425  sgrpidmndm  12775  grpinveu  12865  dfgrp3mlem  12922  ringadd2  13163  cnpnei  13612  txlm  13672  metequiv2  13889  metrest  13899  mulc1cncf  13969  cncfco  13971  dedekindeulemlu  13992  suplociccreex  13995  dedekindicclemlu  14001  ivthinc  14014  cnplimcim  14029  cnplimclemr  14031  limccnpcntop  14037  limccoap  14040  subctctexmid  14632