Theorem reximdv2 3014

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

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-rex 2918

This theorem is referenced by:  ssrexv  3667  ssimaex  6263  nnsuc  7082  oaass  7641  omeulem1  7662  ssnnfi  8179  findcard3  8203  unfilem1  8224  epfrs  8607  alephval3  8933  isfin7-2  9218  fin1a2lem6  9227  fpwwe2lem12  9463  fpwwe2lem13  9464  inawinalem  9511  ico0  12221  ioc0  12222  r19.2uz  14091  climrlim2  14278  iserodd  15540  ramub2  15718  prmgaplem6  15760  pgpssslw  18029  efgrelexlemb  18163  ablfaclem3  18486  unitgrp  18667  lspsneq  19122  lbsextlem4  19161  neissex  20931  iscnp4  21067  nlly2i  21279  llynlly  21280  restnlly  21285  llyrest  21288  nllyrest  21289  llyidm  21291  nllyidm  21292  qtophmeo  21620  cnpflfi  21803  cnextcn  21871  ivthlem3  23222  ovolicc2lem5  23289  dvfsumrlim  23794  itgsubst  23812  lgsquadlem2  25106  footex  25613  opphllem1  25639  oppperpex  25645  outpasch  25647  ushgredgedg  26121  ushgredgedgloop  26123  cusgrfilem2  26352  cmppcmp  29925  eulerpartlemgvv  30438  eulerpartlemgh  30440  erdszelem7  31179  rellysconn  31233  trpredrec  31738  ivthALT  32330  fnessref  32352  phpreu  33393  poimirlem26  33435  itg2gt0cn  33465  frinfm  33530  sstotbnd2  33573  heiborlem3  33612  isdrngo3  33758  dihjat1lem  36717  dvh1dim  36731  dochsatshp  36740  lcfl6  36789  mapdval2N  36919  mapdpglem2  36962  hdmaprnlem10N  37151  pellexlem5  37397  pell14qrss1234  37420  pell1qrss14  37432  pellfundglb  37449  lnr2i  37686  hbtlem6  37699