Theorem reximdva 2652

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  reximddv  2653  reximddv2  2655  dffo4  5859  ctm  7456  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  prarloclemarch  7792  appdivnq  7937  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemloc  7981  archpr  8017  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  archrecpr  8038  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemladdfu  8051  caucvgprlemlim  8055  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemexbt  8080  caucvgprprlemlim  8085  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemlub  8098  archsr  8156  suplocsrlemb  8180  suplocsrlempr  8181  cnegexlem2  8510  bndndx  9574  elpq  10066  qbtwnxr  10709  expnbnd  11122  expnlbnd2  11124  caucvgre  11769  cvg1nlemres  11773  r19.29uz  11780  resqrexlemglsq  11810  resqrexlemga  11811  cau3lem  11903  qdenre  11991  2clim  12092  climcn1  12099  climcn2  12100  climsqz  12126  climsqz2  12127  climcau  12138  divcnv  12289  divalglemex  12714  dvdsbnd  12758  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlembi  12807  lcmgcdlem  12880  divgcdcoprmex  12905  exprmfct  12942  prmdvdsfz  12943  pclemub  13095  pc2dvds  13138  pcprmpw  13142  dvdsprmpweqle  13145  infpnlem2  13168  prmunb  13170  ennnfonelemhom  13364  ctinf  13379  sgrpidmndm  13792  grpinveu  13902  dfgrp3mlem  13962  ringadd2  14439  znunit  15103  cnpnei  15478  txlm  15538  metequiv2  15755  metrest  15765  mulc1cncf  15848  cncfco  15850  dedekindeulemlu  15880  suplociccreex  15883  dedekindicclemlu  15889  ivthinc  15902  cnplimcim  15926  cnplimclemr  15928  limccnpcntop  15934  limccoap  15937  elply2  15994  clwwlkn1loopb  16899  subctctexmid  17268