Theorem reximdva 2493

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  ∃wrex 2376

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380  df-rex 2381

This theorem is referenced by:  reximddv  2494  reximddv2  2496  dffo4  5500  ctm  6909  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  prarloclemarch  7127  appdivnq  7272  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemloc  7316  archpr  7352  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemopu  7357  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  archrecpr  7373  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemopu  7380  caucvgprlemladdfu  7386  caucvgprlemlim  7390  caucvgprprlemml  7403  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemexbt  7415  caucvgprprlemlim  7420  archsr  7477  cnegexlem2  7809  bndndx  8828  qbtwnxr  9876  expnbnd  10256  expnlbnd2  10258  caucvgre  10593  cvg1nlemres  10597  r19.29uz  10604  resqrexlemglsq  10634  resqrexlemga  10635  cau3lem  10726  qdenre  10814  2clim  10909  climcn1  10916  climcn2  10917  climsqz  10943  climsqz2  10944  climcau  10955  divcnv  11105  divalglemex  11414  dvdsbnd  11440  bezoutlemzz  11483  bezoutlemaz  11484  bezoutlembz  11485  bezoutlembi  11486  lcmgcdlem  11551  divgcdcoprmex  11576  exprmfct  11611  prmdvdsfz  11612  ennnfonelemhom  11720  ctinf  11735  cnpnei  12169  txlm  12229  metequiv2  12424  metrest  12434  mulc1cncf  12489  cncfco  12491  cnplimcim  12516  limccnpcntop  12520