Theorem reximdv2 3174

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

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

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 3089

This theorem is used by:  reximdvai  3175  reximssdv  3182  ssimaex  6967  nnsuc  7884  oaass  8552  omeulem1  8573  ssnnfi  9168  findcard3  9257  unfilem1  9279  epfrs  9714  alephval3  10117  isfin7-2  10402  fpwwe2lem12  10655  inawinalem  10702  ico0  13448  ioc0  13449  r19.2uz  15443  climrlim2  15638  prmdvdsncoprmbd  16824  iserodd  16933  ramub2  17112  prmgaplem6  17154  ghmqusnsglem2  19414  ghmquskerlem2  19418  ablfaclem3  20222  unitgrp  20530  isdrng5  20923  restnlly  23714  llyrest  23717  nllyrest  23718  llyidm  23720  nllyidm  23721  cnpflfi  24231  cnextcn  24299  ivthlem3  25687  dvfsumrlim  26265  lgsquadlem2  27625  tglnpt3  29009  tglnpt4  29010  oppperpex  29116  outpasch  29120  ushgredgedg  29697  ushgredgedgloop  29699  cusgrfilem2  29924  nsgqusf1olem2  33851  ssmxidl  33885  cmppcmp  34376  eulerpartlemgvv  34895  eulerpartlemgh  34897  fnrelpredd  35604  r1filimi  35619  noinfepfnregs  35666  erdszelem7  35784  rellysconn  35838  ivthALT  36962  fnessref  36984  phpreu  38366  poimirlem26  38403  itg2gt0cn  38432  frinfm  38493  sstotbnd2  38532  heiborlem3  38571  isdrngo3  38717  dihjat1lem  42309  dvh1dim  42323  dochsatshp  42332  mapdpglem2  42554  prjspreln0  43463  pellexlem5  43682  pell14qrss1234  43705  pell1qrss14  43717  lnr2i  43965  hbtlem6  43978  dflim5  44178  tfsconcatrn  44191  naddgeoa  44243  mnuop3d  45103  fvelsetpreimafv  48295  opnneir  49841