Theorem reximdv2 3199

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3070

This theorem is referenced by:  reximdvai  3200  reximssdv  3205  ssrexv  3988  ssimaex  6853  nnsuc  7730  oaass  8392  omeulem1  8413  ssnnfi  8952  ssnnfiOLD  8953  findcard3  9057  unfilem1  9078  epfrs  9489  alephval3  9866  isfin7-2  10152  fpwwe2lem12  10398  inawinalem  10445  ico0  13125  ioc0  13126  r19.2uz  15063  climrlim2  15256  prmdvdsncoprmbd  16431  iserodd  16536  ramub2  16715  prmgaplem6  16757  ablfaclem3  19690  unitgrp  19909  restnlly  22633  llyrest  22636  nllyrest  22637  llyidm  22639  nllyidm  22640  cnpflfi  23150  cnextcn  23218  ivthlem3  24617  dvfsumrlim  25195  lgsquadlem2  26529  oppperpex  27114  outpasch  27116  ushgredgedg  27596  ushgredgedgloop  27598  cusgrfilem2  27823  nsgqusf1olem2  31599  ssmxidl  31642  cmppcmp  31808  eulerpartlemgvv  32343  eulerpartlemgh  32345  fnrelpredd  33061  erdszelem7  33159  rellysconn  33213  ivthALT  34524  fnessref  34546  phpreu  35761  poimirlem26  35803  itg2gt0cn  35832  frinfm  35893  sstotbnd2  35932  heiborlem3  35971  isdrngo3  36117  dihjat1lem  39442  dvh1dim  39456  dochsatshp  39465  mapdpglem2  39687  prjspreln0  40448  pellexlem5  40655  pell14qrss1234  40678  pell1qrss14  40690  lnr2i  40941  hbtlem6  40954  mnuop3d  41889  fvelsetpreimafv  44839  opnneir  46200