Theorem reximdv2 3175

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-rex 3090

This theorem is referenced by:  reximdvai  3176  reximssdv  3183  ssimaex  6956  nnsuc  7868  oaass  8534  omeulem1  8555  ssnnfi  9142  findcard3  9231  unfilem1  9253  epfrs  9688  alephval3  10082  isfin7-2  10368  fpwwe2lem12  10615  inawinalem  10662  ico0  13406  ioc0  13407  r19.2uz  15391  climrlim2  15586  prmdvdsncoprmbd  16774  iserodd  16883  ramub2  17062  prmgaplem6  17104  ghmqusnsglem2  19339  ghmquskerlem2  19343  ablfaclem3  20147  unitgrp  20453  restnlly  23596  llyrest  23599  nllyrest  23600  llyidm  23602  nllyidm  23603  cnpflfi  24113  cnextcn  24181  ivthlem3  25569  dvfsumrlim  26147  lgsquadlem2  27499  tglnpt3  28877  tglnpt4  28878  oppperpex  28980  outpasch  28982  ushgredgedg  29484  ushgredgedgloop  29486  cusgrfilem2  29711  nsgqusf1olem2  33634  ssmxidl  33669  cmppcmp  34160  eulerpartlemgvv  34678  eulerpartlemgh  34680  fnrelpredd  35392  r1filimi  35406  noinfepfnregs  35435  erdszelem7  35555  rellysconn  35609  ivthALT  36703  fnessref  36725  phpreu  38110  poimirlem26  38152  itg2gt0cn  38181  frinfm  38241  sstotbnd2  38280  heiborlem3  38319  isdrngo3  38465  dihjat1lem  42059  dvh1dim  42073  dochsatshp  42082  mapdpglem2  42304  prjspreln0  43198  pellexlem5  43417  pell14qrss1234  43440  pell1qrss14  43452  lnr2i  43700  hbtlem6  43713  dflim5  43913  tfsconcatrn  43926  naddgeoa  43978  mnuop3d  44840  fvelsetpreimafv  47992  opnneir  49537