Theorem reximdv2 3139

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3054

This theorem is referenced by:  reximdvai  3140  reximssdv  3147  ssrexvOLD  4011  ssimaex  6912  nnsuc  7824  oaass  8486  omeulem1  8507  ssnnfi  9093  findcard3  9187  findcard3OLD  9188  unfilem1  9212  epfrs  9646  alephval3  10023  isfin7-2  10309  fpwwe2lem12  10555  inawinalem  10602  ico0  13312  ioc0  13313  r19.2uz  15277  climrlim2  15472  prmdvdsncoprmbd  16656  iserodd  16765  ramub2  16944  prmgaplem6  16986  ghmqusnsglem2  19178  ghmquskerlem2  19182  ablfaclem3  19986  unitgrp  20286  restnlly  23385  llyrest  23388  nllyrest  23389  llyidm  23391  nllyidm  23392  cnpflfi  23902  cnextcn  23970  ivthlem3  25370  dvfsumrlim  25954  lgsquadlem2  27308  oppperpex  28716  outpasch  28718  ushgredgedg  29192  ushgredgedgloop  29194  cusgrfilem2  29420  nsgqusf1olem2  33361  ssmxidl  33421  cmppcmp  33824  eulerpartlemgvv  34343  eulerpartlemgh  34345  fnrelpredd  35055  erdszelem7  35169  rellysconn  35223  ivthALT  36308  fnessref  36330  phpreu  37583  poimirlem26  37625  itg2gt0cn  37654  frinfm  37714  sstotbnd2  37753  heiborlem3  37792  isdrngo3  37938  dihjat1lem  41407  dvh1dim  41421  dochsatshp  41430  mapdpglem2  41652  prjspreln0  42582  pellexlem5  42806  pell14qrss1234  42829  pell1qrss14  42841  lnr2i  43089  hbtlem6  43102  dflim5  43302  tfsconcatrn  43315  naddgeoa  43367  mnuop3d  44244  fvelsetpreimafv  47372  opnneir  48892