Theorem reximdv2 3176

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

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

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 1945

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

This theorem is used by:  reximdvai  3177  reximssdv  3184  frinf  6311  ssimaex  6996  nnsuc  7922  oaass  8600  omeulem1  8621  ssnnfi  9216  findcard3  9305  unfilem1  9328  epfrs  9762  r1filimi  9933  alephval3  10219  isfin7-2  10504  fpwwe2lem12  10757  inawinalem  10804  ico0  13552  ioc0  13553  r19.2uz  15551  climrlim2  15746  prmdvdsncoprmbd  16935  iserodd  17045  ramub2  17224  prmgaplem6  17266  ghmqusnsglem2  19528  ghmquskerlem2  19532  ablfaclem3  20336  unitgrp  20646  isdrng5  21041  restnlly  23834  llyrest  23837  nllyrest  23838  llyidm  23840  nllyidm  23841  cnpflfi  24351  cnextcn  24419  ivthlem3  25807  dvfsumrlim  26384  lgsquadlem2  27741  tglnpt3  29155  tglnpt4  29156  oppperpex  29262  outpasch  29266  ushgredgedg  29843  ushgredgedgloop  29845  cusgrfilem2  30070  nsgqusf1olem2  34049  ssmxidl  34083  cmppcmp  34573  eulerpartlemgvv  35091  eulerpartlemgh  35093  fnrelpredd  35817  noinfepfnregs  35913  erdszelem7  36142  rellysconn  36196  ivthALT  37314  fnessref  37336  phpreu  38732  poimirlem26  38769  itg2gt0cn  38798  sstotbnd2  38911  heiborlem3  38950  isdrngo3  39096  dihjat1lem  42688  dvh1dim  42702  dochsatshp  42711  mapdpglem2  42933  prjspreln0  43841  pellexlem5  44044  pell14qrss1234  44067  pell1qrss14  44079  lnr2i  44321  hbtlem6  44334  dflim5  44534  tfsconcatrn  44547  naddgeoa  44599  mnuop3d  45458  fvelsetpreimafv  48684  opnneir  50236