Theorem reximdva 2566

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2135  ∃wrex 2443

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447  df-rex 2448

This theorem is referenced by:  reximddv  2567  reximddv2  2569  dffo4  5627  ctm  7065  ctssdclemn0  7066  ctssdccl  7067  ctssdc  7069  prarloclemarch  7350  appdivnq  7495  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemloc  7539  archpr  7575  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  archrecpr  7596  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemladdfu  7609  caucvgprlemlim  7613  caucvgprprlemml  7626  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemexbt  7638  caucvgprprlemlim  7643  suplocexprlemmu  7650  suplocexprlemru  7651  suplocexprlemlub  7656  archsr  7714  suplocsrlemb  7738  suplocsrlempr  7739  cnegexlem2  8065  bndndx  9104  elpq  9577  qbtwnxr  10183  expnbnd  10567  expnlbnd2  10569  caucvgre  10909  cvg1nlemres  10913  r19.29uz  10920  resqrexlemglsq  10950  resqrexlemga  10951  cau3lem  11042  qdenre  11130  2clim  11228  climcn1  11235  climcn2  11236  climsqz  11262  climsqz2  11263  climcau  11274  divcnv  11424  divalglemex  11844  dvdsbnd  11874  bezoutlemzz  11920  bezoutlemaz  11921  bezoutlembz  11922  bezoutlembi  11923  lcmgcdlem  11988  divgcdcoprmex  12013  exprmfct  12049  prmdvdsfz  12050  pclemub  12196  pc2dvds  12238  pcprmpw  12242  dvdsprmpweqle  12245  ennnfonelemhom  12285  ctinf  12300  cnpnei  12760  txlm  12820  metequiv2  13037  metrest  13047  mulc1cncf  13117  cncfco  13119  dedekindeulemlu  13140  suplociccreex  13143  dedekindicclemlu  13149  ivthinc  13162  cnplimcim  13177  cnplimclemr  13179  limccnpcntop  13185  limccoap  13188  subctctexmid  13715