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 1947	. 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 1809   ∈ wcel 2143  ∃wrex 3089

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

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

This theorem is referenced by:  reximdvai  3176  reximssdv  3183  ssimaex  6968  nnsuc  7881  oaass  8547  omeulem1  8568  ssnnfi  9155  findcard3  9244  unfilem1  9266  epfrs  9701  alephval3  10095  isfin7-2  10381  fpwwe2lem12  10628  inawinalem  10675  ico0  13419  ioc0  13420  r19.2uz  15405  climrlim2  15600  prmdvdsncoprmbd  16787  iserodd  16896  ramub2  17075  prmgaplem6  17117  ghmqusnsglem2  19352  ghmquskerlem2  19356  ablfaclem3  20160  unitgrp  20466  restnlly  23620  llyrest  23623  nllyrest  23624  llyidm  23626  nllyidm  23627  cnpflfi  24137  cnextcn  24205  ivthlem3  25593  dvfsumrlim  26171  lgsquadlem2  27526  tglnpt3  28908  tglnpt4  28909  oppperpex  29015  outpasch  29018  ushgredgedg  29560  ushgredgedgloop  29562  cusgrfilem2  29787  nsgqusf1olem2  33704  ssmxidl  33738  cmppcmp  34229  eulerpartlemgvv  34747  eulerpartlemgh  34749  fnrelpredd  35463  r1filimi  35478  noinfepfnregs  35526  erdszelem7  35670  rellysconn  35724  ivthALT  36827  fnessref  36849  phpreu  38236  poimirlem26  38278  itg2gt0cn  38307  frinfm  38367  sstotbnd2  38406  heiborlem3  38445  isdrngo3  38591  dihjat1lem  42183  dvh1dim  42197  dochsatshp  42206  mapdpglem2  42428  prjspreln0  43324  pellexlem5  43543  pell14qrss1234  43566  pell1qrss14  43578  lnr2i  43826  hbtlem6  43839  dflim5  44039  tfsconcatrn  44052  naddgeoa  44104  mnuop3d  44964  fvelsetpreimafv  48119  opnneir  49668