Theorem reximdv2 3195

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 3076	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3076	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 299	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-rex 3076

This theorem is referenced by:  reximssdv  3200  ssrexv  3959  ssimaex  6737  nnsuc  7596  oaass  8197  omeulem1  8218  ssnnfi  8739  findcard3  8794  unfilem1  8815  epfrs  9206  alephval3  9570  isfin7-2  9856  fpwwe2lem12  10102  inawinalem  10149  ico0  12825  ioc0  12826  r19.2uz  14759  climrlim2  14952  prmdvdsncoprmbd  16122  iserodd  16227  ramub2  16405  prmgaplem6  16447  ablfaclem3  19277  unitgrp  19488  restnlly  22182  llyrest  22185  nllyrest  22186  llyidm  22188  nllyidm  22189  cnpflfi  22699  cnextcn  22767  ivthlem3  24153  dvfsumrlim  24730  lgsquadlem2  26064  oppperpex  26646  outpasch  26648  ushgredgedg  27118  ushgredgedgloop  27120  cusgrfilem2  27345  nsgqusf1olem2  31120  ssmxidl  31163  cmppcmp  31329  eulerpartlemgvv  31862  eulerpartlemgh  31864  fnrelpredd  32590  erdszelem7  32675  rellysconn  32729  trpredrec  33324  ivthALT  34095  fnessref  34117  phpreu  35343  poimirlem26  35385  itg2gt0cn  35414  frinfm  35475  sstotbnd2  35514  heiborlem3  35553  isdrngo3  35699  dihjat1lem  39026  dvh1dim  39040  dochsatshp  39049  mapdpglem2  39271  prjspreln0  39967  pellexlem5  40169  pell14qrss1234  40192  pell1qrss14  40204  lnr2i  40455  hbtlem6  40468  mnuop3d  41374  fvelsetpreimafv  44294  opnneir  45604