Theorem reximdv2 3173

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3088

This theorem is used by:  reximdvai  3174  reximssdv  3181  ssimaex  6962  nnsuc  7884  oaass  8553  omeulem1  8574  ssnnfi  9169  findcard3  9258  unfilem1  9281  epfrs  9716  r1filimi  9884  alephval3  10170  isfin7-2  10455  fpwwe2lem12  10708  inawinalem  10755  ico0  13503  ioc0  13504  r19.2uz  15499  climrlim2  15694  prmdvdsncoprmbd  16883  iserodd  16993  ramub2  17172  prmgaplem6  17214  ghmqusnsglem2  19475  ghmquskerlem2  19479  ablfaclem3  20283  unitgrp  20593  isdrng5  20988  restnlly  23781  llyrest  23784  nllyrest  23785  llyidm  23787  nllyidm  23788  cnpflfi  24298  cnextcn  24366  ivthlem3  25754  dvfsumrlim  26331  lgsquadlem2  27690  tglnpt3  29104  tglnpt4  29105  oppperpex  29211  outpasch  29215  ushgredgedg  29792  ushgredgedgloop  29794  cusgrfilem2  30019  nsgqusf1olem2  33947  ssmxidl  33981  cmppcmp  34472  eulerpartlemgvv  34991  eulerpartlemgh  34993  fnrelpredd  35699  noinfepfnregs  35773  erdszelem7  35931  rellysconn  35985  ivthALT  37093  fnessref  37115  phpreu  38495  poimirlem26  38532  itg2gt0cn  38561  frinfm  38637  sstotbnd2  38676  heiborlem3  38715  isdrngo3  38861  dihjat1lem  42453  dvh1dim  42467  dochsatshp  42476  mapdpglem2  42698  prjspreln0  43599  pellexlem5  43793  pell14qrss1234  43816  pell1qrss14  43828  lnr2i  44076  hbtlem6  44089  dflim5  44289  tfsconcatrn  44302  naddgeoa  44354  mnuop3d  45214  fvelsetpreimafv  48413  opnneir  49959