Theorem reximdv2 3273

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)

Hypothesis

Ref	Expression
reximdv2.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))

Assertion

Ref	Expression
reximdv2	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem reximdv2

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	eximdv 1918	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3146	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3146	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 298	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-rex 3146

This theorem is referenced by:  reximssdv  3278  ssrexv  4036  ssimaex  6750  nnsuc  7599  oaass  8189  omeulem1  8210  ssnnfi  8739  findcard3  8763  unfilem1  8784  epfrs  9175  alephval3  9538  isfin7-2  9820  fpwwe2lem13  10066  inawinalem  10113  ico0  12787  ioc0  12788  r19.2uz  14713  climrlim2  14906  iserodd  16174  ramub2  16352  prmgaplem6  16394  ablfaclem3  19211  unitgrp  19419  restnlly  22092  llyrest  22095  nllyrest  22096  llyidm  22098  nllyidm  22099  cnpflfi  22609  cnextcn  22677  ivthlem3  24056  dvfsumrlim  24630  lgsquadlem2  25959  oppperpex  26541  outpasch  26543  ushgredgedg  27013  ushgredgedgloop  27015  cusgrfilem2  27240  ssmxidl  30981  cmppcmp  31124  eulerpartlemgvv  31636  eulerpartlemgh  31638  erdszelem7  32446  rellysconn  32500  trpredrec  33079  ivthALT  33685  fnessref  33707  phpreu  34878  poimirlem26  34920  itg2gt0cn  34949  frinfm  35012  sstotbnd2  35054  heiborlem3  35093  isdrngo3  35239  dihjat1lem  38566  dvh1dim  38580  dochsatshp  38589  mapdpglem2  38811  prjspreln0  39266  pellexlem5  39437  pell14qrss1234  39460  pell1qrss14  39472  lnr2i  39723  hbtlem6  39736  mnuop3d  40614  fvelsetpreimafv  43554