Theorem reximdv2 3146

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3061

This theorem is referenced by:  reximdvai  3147  reximssdv  3154  ssrexvOLD  4007  ssimaex  6919  nnsuc  7826  oaass  8488  omeulem1  8509  ssnnfi  9094  findcard3  9183  unfilem1  9205  epfrs  9640  alephval3  10020  isfin7-2  10306  fpwwe2lem12  10553  inawinalem  10600  ico0  13307  ioc0  13308  r19.2uz  15275  climrlim2  15470  prmdvdsncoprmbd  16654  iserodd  16763  ramub2  16942  prmgaplem6  16984  ghmqusnsglem2  19210  ghmquskerlem2  19214  ablfaclem3  20018  unitgrp  20319  restnlly  23426  llyrest  23429  nllyrest  23430  llyidm  23432  nllyidm  23433  cnpflfi  23943  cnextcn  24011  ivthlem3  25410  dvfsumrlim  25994  lgsquadlem2  27348  oppperpex  28825  outpasch  28827  ushgredgedg  29302  ushgredgedgloop  29304  cusgrfilem2  29530  nsgqusf1olem2  33495  ssmxidl  33555  cmppcmp  34015  eulerpartlemgvv  34533  eulerpartlemgh  34535  fnrelpredd  35247  r1filimi  35259  noinfepfnregs  35288  erdszelem7  35391  rellysconn  35445  ivthALT  36529  fnessref  36551  phpreu  37801  poimirlem26  37843  itg2gt0cn  37872  frinfm  37932  sstotbnd2  37971  heiborlem3  38010  isdrngo3  38156  dihjat1lem  41684  dvh1dim  41698  dochsatshp  41707  mapdpglem2  41929  prjspreln0  42848  pellexlem5  43071  pell14qrss1234  43094  pell1qrss14  43106  lnr2i  43354  hbtlem6  43367  dflim5  43567  tfsconcatrn  43580  naddgeoa  43632  mnuop3d  44508  fvelsetpreimafv  47629  opnneir  49148