Theorem reximdva 2534

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 114	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 2532	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∃wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  reximddv  2535  reximddv2  2537  dffo4  5568  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  prarloclemarch  7226  appdivnq  7371  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  archrecpr  7472  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemladdfu  7485  caucvgprlemlim  7489  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemexbt  7514  caucvgprprlemlim  7519  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemlub  7532  archsr  7590  suplocsrlemb  7614  suplocsrlempr  7615  cnegexlem2  7938  bndndx  8976  qbtwnxr  10035  expnbnd  10415  expnlbnd2  10417  caucvgre  10753  cvg1nlemres  10757  r19.29uz  10764  resqrexlemglsq  10794  resqrexlemga  10795  cau3lem  10886  qdenre  10974  2clim  11070  climcn1  11077  climcn2  11078  climsqz  11104  climsqz2  11105  climcau  11116  divcnv  11266  divalglemex  11619  dvdsbnd  11645  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  bezoutlembi  11693  lcmgcdlem  11758  divgcdcoprmex  11783  exprmfct  11818  prmdvdsfz  11819  ennnfonelemhom  11928  ctinf  11943  cnpnei  12388  txlm  12448  metequiv2  12665  metrest  12675  mulc1cncf  12745  cncfco  12747  dedekindeulemlu  12768  suplociccreex  12771  dedekindicclemlu  12777  ivthinc  12790  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccoap  12816  subctctexmid  13196