Theorem reximdv2 2997

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

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902

This theorem is referenced by:  ssrexv  3630  ssimaex  6173  nnsuc  6974  oaass  7528  omeulem1  7549  ssnnfi  8064  findcard3  8088  unfilem1  8109  epfrs  8490  alephval3  8816  isfin7-2  9101  fin1a2lem6  9110  fpwwe2lem12  9342  fpwwe2lem13  9343  inawinalem  9390  ico0  12092  ioc0  12093  r19.2uz  13939  climrlim2  14126  iserodd  15378  ramub2  15556  prmgaplem6  15598  pgpssslw  17852  efgrelexlemb  17986  ablfaclem3  18309  unitgrp  18490  lspsneq  18943  lbsextlem4  18982  neissex  20741  iscnp4  20877  nlly2i  21089  llynlly  21090  restnlly  21095  llyrest  21098  nllyrest  21099  llyidm  21101  nllyidm  21102  qtophmeo  21430  cnpflfi  21613  cnextcn  21681  ivthlem3  23029  ovolicc2lem5  23096  dvfsumrlim  23598  itgsubst  23616  lgsquadlem2  24906  footex  25413  opphllem1  25439  oppperpex  25445  outpasch  25447  nbgraf1olem5  25974  cusgrafilem2  26008  cmppcmp  29253  eulerpartlemgvv  29765  eulerpartlemgh  29767  erdszelem7  30433  rellyscon  30487  trpredrec  30982  ivthALT  31500  fnessref  31522  phpreu  32563  poimirlem26  32605  itg2gt0cn  32635  frinfm  32700  sstotbnd2  32743  heiborlem3  32782  isdrngo3  32928  dihjat1lem  35735  dvh1dim  35749  dochsatshp  35758  lcfl6  35807  mapdval2N  35937  mapdpglem2  35980  hdmaprnlem10N  36169  pellexlem5  36415  pell14qrss1234  36438  pell1qrss14  36450  pellfundglb  36467  lnr2i  36705  hbtlem6  36718  ushgredgedga  40456  ushgredgedgaloop  40458  cusgrfilem2  40672