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  6158  nnsuc  6952  oaass  7506  omeulem1  7527  ssnnfi  8042  findcard3  8066  unfilem1  8087  epfrs  8468  alephval3  8794  isfin7-2  9079  fin1a2lem6  9088  fpwwe2lem12  9320  fpwwe2lem13  9321  inawinalem  9368  ico0  12051  ioc0  12052  r19.2uz  13888  climrlim2  14075  iserodd  15327  ramub2  15505  prmgaplem6  15547  pgpssslw  17801  efgrelexlemb  17935  ablfaclem3  18258  unitgrp  18439  lspsneq  18892  lbsextlem4  18931  neissex  20689  iscnp4  20825  nlly2i  21037  llynlly  21038  restnlly  21043  llyrest  21046  nllyrest  21047  llyidm  21049  nllyidm  21050  qtophmeo  21378  cnpflfi  21561  cnextcn  21629  ivthlem3  22974  ovolicc2lem5  23041  dvfsumrlim  23543  itgsubst  23561  lgsquadlem2  24851  footex  25359  opphllem1  25385  oppperpex  25391  outpasch  25393  nbgraf1olem5  25768  cusgrafilem2  25802  cmppcmp  29047  eulerpartlemgvv  29559  eulerpartlemgh  29561  erdszelem7  30227  rellyscon  30281  trpredrec  30776  ivthALT  31294  fnessref  31316  phpreu  32357  poimirlem26  32399  itg2gt0cn  32429  frinfm  32494  sstotbnd2  32537  heiborlem3  32576  isdrngo3  32722  dihjat1lem  35529  dvh1dim  35543  dochsatshp  35552  lcfl6  35601  mapdval2N  35731  mapdpglem2  35774  hdmaprnlem10N  35963  pellexlem5  36209  pell14qrss1234  36232  pell1qrss14  36244  pellfundglb  36261  lnr2i  36499  hbtlem6  36512  ushgredgedga  40448  ushgredgedgaloop  40450  cusgrfilem2  40664