Theorem reximdv2 3161

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

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3067

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 3068

This theorem is referenced by:  reximdvai  3162  reximssdv  3170  ssrexv  4051  ssimaex  6988  nnsuc  7896  oaass  8590  omeulem1  8611  ssnnfi  9202  ssnnfiOLD  9203  findcard3  9318  findcard3OLD  9319  unfilem1  9343  epfrs  9764  alephval3  10143  isfin7-2  10429  fpwwe2lem12  10675  inawinalem  10722  ico0  13412  ioc0  13413  r19.2uz  15340  climrlim2  15533  prmdvdsncoprmbd  16708  iserodd  16813  ramub2  16992  prmgaplem6  17034  ghmquskerlem2  19250  ablfaclem3  20058  unitgrp  20336  restnlly  23414  llyrest  23417  nllyrest  23418  llyidm  23420  nllyidm  23421  cnpflfi  23931  cnextcn  23999  ivthlem3  25410  dvfsumrlim  25994  lgsquadlem2  27342  oppperpex  28585  outpasch  28587  ushgredgedg  29070  ushgredgedgloop  29072  cusgrfilem2  29298  nsgqusf1olem2  33157  ghmqusnsglem2  33163  ssmxidl  33220  cmppcmp  33500  eulerpartlemgvv  34037  eulerpartlemgh  34039  fnrelpredd  34753  erdszelem7  34848  rellysconn  34902  ivthALT  35860  fnessref  35882  phpreu  37118  poimirlem26  37160  itg2gt0cn  37189  frinfm  37249  sstotbnd2  37288  heiborlem3  37327  isdrngo3  37473  dihjat1lem  40941  dvh1dim  40955  dochsatshp  40964  mapdpglem2  41186  prjspreln0  42082  pellexlem5  42302  pell14qrss1234  42325  pell1qrss14  42337  lnr2i  42589  hbtlem6  42602  dflim5  42807  tfsconcatrn  42820  naddgeoa  42873  mnuop3d  43757  fvelsetpreimafv  46774  opnneir  48021