Theorem reximdva 2568

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  ∃wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  reximddv  2569  reximddv2  2571  dffo4  5633  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  prarloclemarch  7359  appdivnq  7504  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemloc  7548  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  archrecpr  7605  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemladdfu  7618  caucvgprlemlim  7622  caucvgprprlemml  7635  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemexbt  7647  caucvgprprlemlim  7652  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemlub  7665  archsr  7723  suplocsrlemb  7747  suplocsrlempr  7748  cnegexlem2  8074  bndndx  9113  elpq  9586  qbtwnxr  10193  expnbnd  10578  expnlbnd2  10580  caucvgre  10923  cvg1nlemres  10927  r19.29uz  10934  resqrexlemglsq  10964  resqrexlemga  10965  cau3lem  11056  qdenre  11144  2clim  11242  climcn1  11249  climcn2  11250  climsqz  11276  climsqz2  11277  climcau  11288  divcnv  11438  divalglemex  11859  dvdsbnd  11889  bezoutlemzz  11935  bezoutlemaz  11936  bezoutlembz  11937  bezoutlembi  11938  lcmgcdlem  12009  divgcdcoprmex  12034  exprmfct  12070  prmdvdsfz  12071  pclemub  12219  pc2dvds  12261  pcprmpw  12265  dvdsprmpweqle  12268  infpnlem2  12290  prmunb  12292  ennnfonelemhom  12348  ctinf  12363  cnpnei  12859  txlm  12919  metequiv2  13136  metrest  13146  mulc1cncf  13216  cncfco  13218  dedekindeulemlu  13239  suplociccreex  13242  dedekindicclemlu  13248  ivthinc  13261  cnplimcim  13276  cnplimclemr  13278  limccnpcntop  13284  limccoap  13287  subctctexmid  13881