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  6917  nnsuc  7826  oaass  8487  omeulem1  8508  ssnnfi  9095  findcard3  9184  unfilem1  9206  epfrs  9641  alephval3  10021  isfin7-2  10307  fpwwe2lem12  10554  inawinalem  10601  ico0  13308  ioc0  13309  r19.2uz  15276  climrlim2  15471  prmdvdsncoprmbd  16655  iserodd  16764  ramub2  16943  prmgaplem6  16985  ghmqusnsglem2  19214  ghmquskerlem2  19218  ablfaclem3  20022  unitgrp  20321  restnlly  23425  llyrest  23428  nllyrest  23429  llyidm  23431  nllyidm  23432  cnpflfi  23942  cnextcn  24010  ivthlem3  25398  dvfsumrlim  25979  lgsquadlem2  27332  oppperpex  28809  outpasch  28811  ushgredgedg  29286  ushgredgedgloop  29288  cusgrfilem2  29514  nsgqusf1olem2  33479  ssmxidl  33539  cmppcmp  34008  eulerpartlemgvv  34526  eulerpartlemgh  34528  fnrelpredd  35240  r1filimi  35252  noinfepfnregs  35282  erdszelem7  35385  rellysconn  35439  ivthALT  36523  fnessref  36545  phpreu  37916  poimirlem26  37958  itg2gt0cn  37987  frinfm  38047  sstotbnd2  38086  heiborlem3  38125  isdrngo3  38271  dihjat1lem  41865  dvh1dim  41879  dochsatshp  41888  mapdpglem2  42110  prjspreln0  43041  pellexlem5  43264  pell14qrss1234  43287  pell1qrss14  43299  lnr2i  43547  hbtlem6  43560  dflim5  43760  tfsconcatrn  43773  naddgeoa  43825  mnuop3d  44701  fvelsetpreimafv  47821  opnneir  49340