Theorem reximdv2 3158

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1773   ∈ wcel 2098  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3065

This theorem is referenced by:  reximdvai  3159  reximssdv  3166  ssrexv  4046  ssimaex  6970  nnsuc  7870  oaass  8562  omeulem1  8583  ssnnfi  9171  ssnnfiOLD  9172  findcard3  9287  findcard3OLD  9288  unfilem1  9312  epfrs  9728  alephval3  10107  isfin7-2  10393  fpwwe2lem12  10639  inawinalem  10686  ico0  13376  ioc0  13377  r19.2uz  15304  climrlim2  15497  prmdvdsncoprmbd  16672  iserodd  16777  ramub2  16956  prmgaplem6  16998  ablfaclem3  20009  unitgrp  20285  restnlly  23341  llyrest  23344  nllyrest  23345  llyidm  23347  nllyidm  23348  cnpflfi  23858  cnextcn  23926  ivthlem3  25337  dvfsumrlim  25921  lgsquadlem2  27269  oppperpex  28512  outpasch  28514  ushgredgedg  28994  ushgredgedgloop  28996  cusgrfilem2  29222  nsgqusf1olem2  33031  ghmquskerlem2  33036  ssmxidl  33096  cmppcmp  33368  eulerpartlemgvv  33905  eulerpartlemgh  33907  fnrelpredd  34621  erdszelem7  34716  rellysconn  34770  ivthALT  35728  fnessref  35750  phpreu  36985  poimirlem26  37027  itg2gt0cn  37056  frinfm  37116  sstotbnd2  37155  heiborlem3  37194  isdrngo3  37340  dihjat1lem  40812  dvh1dim  40826  dochsatshp  40835  mapdpglem2  41057  prjspreln0  41929  pellexlem5  42149  pell14qrss1234  42172  pell1qrss14  42184  lnr2i  42436  hbtlem6  42449  dflim5  42655  tfsconcatrn  42668  naddgeoa  42721  mnuop3d  43606  fvelsetpreimafv  46627  opnneir  47813