Theorem reximdv2 3148

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximdvai  3149  reximssdv  3156  ssrexvOLD  3996  ssimaex  6919  nnsuc  7828  oaass  8489  omeulem1  8510  ssnnfi  9097  findcard3  9186  unfilem1  9208  epfrs  9643  alephval3  10023  isfin7-2  10309  fpwwe2lem12  10556  inawinalem  10603  ico0  13335  ioc0  13336  r19.2uz  15305  climrlim2  15500  prmdvdsncoprmbd  16688  iserodd  16797  ramub2  16976  prmgaplem6  17018  ghmqusnsglem2  19247  ghmquskerlem2  19251  ablfaclem3  20055  unitgrp  20354  restnlly  23457  llyrest  23460  nllyrest  23461  llyidm  23463  nllyidm  23464  cnpflfi  23974  cnextcn  24042  ivthlem3  25430  dvfsumrlim  26008  lgsquadlem2  27358  oppperpex  28835  outpasch  28837  ushgredgedg  29312  ushgredgedgloop  29314  cusgrfilem2  29540  nsgqusf1olem2  33489  ssmxidl  33549  cmppcmp  34018  eulerpartlemgvv  34536  eulerpartlemgh  34538  fnrelpredd  35250  r1filimi  35262  noinfepfnregs  35292  erdszelem7  35395  rellysconn  35449  ivthALT  36533  fnessref  36555  phpreu  37939  poimirlem26  37981  itg2gt0cn  38010  frinfm  38070  sstotbnd2  38109  heiborlem3  38148  isdrngo3  38294  dihjat1lem  41888  dvh1dim  41902  dochsatshp  41911  mapdpglem2  42133  prjspreln0  43056  pellexlem5  43279  pell14qrss1234  43302  pell1qrss14  43314  lnr2i  43562  hbtlem6  43575  dflim5  43775  tfsconcatrn  43788  naddgeoa  43840  mnuop3d  44716  fvelsetpreimafv  47859  opnneir  49394